John and Freek, I'm over 1000 lines of miz3 axiomatic Hilbert code
(below), and I my code now (after the beginning) only uses the set
theoretic B IN open_int (A, C) instead of the Between (A,B,C) .
I found what may be a bug in miz3: I could not prove my thms B3' and
B4' in the way I proved thms B1' and B2'.
--
Best,
Bill
(* Paste in these 2 commands
cd hol_light; ocaml
#use "hol.ml";;
#load "unix.cma";;
loadt "miz3/miz3.ml";;
and then paste in the following file. *)
(* ================================================================= *)
(* HOL Light Hilbert geometry axiomatic proofs. *)
(* ================================================================= *)
(* Thanks to Mizar folks who wrote an influential language I was able
to learn, Freek Wiedijk, who wrote the miz3 port of Mizar to HOL
Light, and especially John Harrison, who came up with the entire
framework here of porting my axiomatic proofs to HOL Light. *)
horizon := 0;;
new_type("point",0);;
new_type_abbrev("point_set",`:point->bool`);;
new_constant("Between",`:point#point#point->bool`);;
new_constant("===",`:point#point->point#point->bool`);;
new_constant("Line",`:point_set->bool`);;
parse_as_infix("===",(12, "right"));;
parse_as_infix("cong",(12, "right"));;
parse_as_infix("same_side",(12, "right"));;
parse_as_infix("int_angle",(12, "right"));;
let Interval_DEF = new_definition
`!A B X. open_int (A,B) X <=> Between (A,X,B)`;;
let Collinear_DEF = new_definition
`Collinear (A,B,C) <=>
?l. Line l /\ A IN l /\ B IN l /\ C IN l`;;
let same_side_DEF = new_definition
`A,B same_side l <=>
Line l /\ ~(?X. (X IN l) /\ X IN open_int (A,B))`;;
let Ray_DEF = new_definition
`!A B X. ray (A,B) X <=> ~(A = B) /\ Collinear (A,B,X) /\ ~(A IN open_int
(X,B))`;;
let cong_DEF = new_definition
`A,B,C cong X,Y,Z <=>
A,B === X,Y /\ A,C === X,Z /\ B,C === Y,Z`;;
let is_ordered_DEF = new_definition
`is_ordered (A,B,C,D) <=>
B IN open_int (A,C) /\ B IN open_int (A,D) /\ C IN open_int (A,D) /\ C IN
open_int (B,D)`;;
let Reflexive_relation_DEF = new_definition
`Reflexive_Property <=>
!l A. Line l /\ ~(A IN l) ==> A,A same_side l`;;
let Symmetric_relation_DEF = new_definition
`Symmetric_Property <=>
!l A B. Line l /\ ~(A IN l) /\ ~(B IN l) ==>
A,B same_side l ==> B,A same_side l`;;
let Transitive_relation_DEF = new_definition
`Transitive_Property <=>
!l A B C.
Line l /\ ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) ==>
A,B same_side l /\ B,C same_side l ==> A,C same_side l`;;
(*
exec GOAL_TAC;
p();;
let Angle_DEF = new_definition
`!A O B. Angle (A,O,B) = if Collinear (A,O,B) then {} else
{ray (O,A), ray (O,B)}`;;
*)
let InteriorAngle_DEF = new_definition
`!A O B P.
P int_angle A,O,B <=> ~Collinear (A,O,B) /\ ?a b.
Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\
~(P IN a) /\ ~(P IN b) /\ P,B same_side a /\ P,A same_side b`;;
(* ------------------------------------------------------------------------- *)
(* The axioms. *)
(* ------------------------------------------------------------------------- *)
let I1 = new_axiom
`!A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;;
let I2 = new_axiom
`!l. ? A B. Line l /\ A IN l /\ B IN l /\ ~(A = B)`;;
let I3 = new_axiom
`?A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
~Collinear (A,B,C)`;;
let B1 = new_axiom
`! A B C. Between (A,B,C) ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
Between (C,B,A) /\ Collinear (A,B,C)`;;
let B2 = new_axiom
`! A B. ~(A = B) ==> ?C. Between (A,B,C)`;;
let B3 = new_axiom
`!A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear (A,B,C)
==> (Between (A,B,C) \/ Between (B,C,A) \/ Between (C,A,B)) /\
~(Between (A,B,C) /\ Between (B,C,A)) /\
~(Between (A,B,C) /\ Between (C,A,B)) /\
~(Between (B,C,A) /\ Between (C,A,B))`;;
let B4 = new_axiom
`!l A B C. Line l /\ ~Collinear (A,B,C) /\
~(A IN l) /\ ~(B IN l) /\ ~(C IN l) /\
(?X. X IN l /\ Between (A,X,C)) ==>
(?Y. Y IN l /\ Between (A,Y,B)) \/ (?Y. Y IN l /\ Between (B,Y,C))`;;
let B1' = thm `;
!A B C. B IN open_int (A,C) ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
B IN open_int (C,A) /\ Collinear (A,B,C)
by IN, Interval_DEF, B1`;;
let B2' = thm `;
!A B. ~(A = B) ==> ?C. B IN open_int (A,C)
by IN, Interval_DEF, B2`;;
let B3' = thm `;
let A B C be point;
assume ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear (A,B,C) [H1];
thus (B IN open_int (A,C) \/ C IN open_int (B,A) \/ A IN open_int (C,B)) /\
~(B IN open_int (A,C) /\ C IN open_int (B,A)) /\
~(B IN open_int (A,C) /\ A IN open_int (C,B)) /\
~(C IN open_int (B,A) /\ A IN open_int (C,B))
proof
qed by H1, IN, Interval_DEF, B3`;;
let B4' = thm `;
let l be point_set;
let A B C be point;
assume Line l /\ ~Collinear (A,B,C) /\
~(A IN l) /\ ~(B IN l) /\ ~(C IN l) /\
(?X. X IN l /\ X IN open_int (A,C)) [H1];
thus (?Y. Y IN l /\ Y IN open_int (A,B)) \/ (?Y. Y IN l /\ Y IN open_int
(B,C))
proof
Line l /\ ~Collinear (A,B,C) /\
~(A IN l) /\ ~(B IN l) /\ ~(C IN l) /\
(?X. X IN l /\ Between (A,X,C)) by H1, IN, Interval_DEF;
(?Y. Y IN l /\ Between (A,Y,B)) \/ (?Y. Y IN l /\ Between (B,Y,C)) by -,
B4;
qed by -, IN, Interval_DEF`;;
let BiggerThanSingleton_THM = thm `;
let p be A->bool;
let x be A;
assume x IN p [H1];
assume ~(p = {x}) [H2];
thus ?a . a IN p /\ ~(a = x)
proof
{x} SUBSET p by H1, SING_SUBSET;
~(p SUBSET {x}) by -, H2, SUBSET_ANTISYM;
consider a such that
a IN p /\ ~(a IN {x}) [X1] by -, SUBSET;
~(a = x) by -, IN_SING;
qed by -, X1`;;
let DisjointOneNotOther_THM = thm `;
let x be A;
let l m be A->bool;
assume l INTER m = {} [H1];
assume x IN m [H2];
thus ~(x IN l)
proof
assume (x IN l);
x IN l INTER m by -, H2, IN_INTER;
F by -, NOT_IN_EMPTY, H1;
qed by -`;;
let IntersectionSingletonOneNotOther_THM = thm `;
let e x be A;
let l m be A->bool;
assume l INTER m = {x} [H1];
assume e IN l [H2];
assume ~(e = x) [H3];
thus ~(e IN m)
proof
assume e IN m;
e IN l INTER m by H2, -, IN_INTER;
e = x by -, H1, IN_SING;
F by -, H3;
qed by -`;;
let EquivIntersectionHelp_THM = thm `;
let a x be A;
let l m be A->bool;
assume l INTER m = {x} [H1];
assume a IN m DELETE x [H2];
thus ~(a IN l)
proof
a IN m /\ ~(a = x) [X1] by H2, IN_DELETE;
qed by -, H1, H2, IntersectionSingletonOneNotOther_THM`;;
let DoubleSubsetEqual_THM = thm `;
let s t be A->bool;
assume s SUBSET t [H1];
assume t SUBSET s [H2];
thus s = t
proof
!x:A. x IN s ==> x IN t [sSt] by H1, SUBSET;
!x:A. x IN t ==> x IN s [tSs] by H2, SUBSET;
!x:A. x IN s <=> x IN t [sEt] by sSt, tSs;
s = t by -, EXTENSION;
qed by -`;;
let CollinearSymmetry_THM = thm `;
let A B C be point;
assume Collinear (A,B,C) [H1];
thus Collinear (A,C,B) /\ Collinear (B,A,C) /\ Collinear (B,C,A) /\
Collinear (C,A,B) /\ Collinear (C,B,A)
proof
consider l such that
Line l /\ A IN l /\ B IN l /\ C IN l by H1, Collinear_DEF;
qed by -, Collinear_DEF`;;
let OnePointImpliesAnother_THM = thm `;
let P be point;
thus ?Q:point. ~(Q = P)
proof
consider A B C such that
~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear (A,B,C) [X1] by I3;
cases;
suppose B = P;
~(A = B) by -, X1;
qed by -;
suppose ~(B = P);
qed by -;
end`;;
let ExistsPointOffLine_THM = thm `;
let l be point_set;
assume Line l [H1];
thus ?Q:point. ~(Q IN l)
proof
consider A B C such that
~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear (A,B,C) [useI3] by I3;
cases;
suppose ~(A IN l) \/ ~(B IN l) \/ ~(C IN l);
qed by -;
suppose (A IN l) /\ (B IN l) /\ (C IN l);
Collinear (A,B,C) by H1, -, Collinear_DEF;
F by -, useI3;
qed by -;
end`;;
let B4'' = thm `;
let l be point_set;
let A B C be point;
assume Line l [H0];
assume ~Collinear (A,B,C) /\ ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) [H1];
assume A,B same_side l /\ B,C same_side l [H2];
thus A,C same_side l
proof
~(?Y. Y IN l /\ Y IN open_int (A,B)) /\
~(?Y. Y IN l /\ Y IN open_int (B,C)) ==>
~(?X. X IN l /\ X IN open_int (A,C)) by H0, H1, B4';
qed by -, H1, H2, IN, same_side_DEF`;;
let BetweenLinear_THM = thm `;
let A B C be point;
let m be point_set;
assume Line m /\ A IN m /\ C IN m [H1];
assume B IN open_int (A,C) \/ C IN open_int (B,A) \/ A IN open_int (C,B)
[H2];
thus B IN m
proof
~(A = C) /\
(Collinear (A,B,C) \/ Collinear (B,C,A) \/ Collinear (C,A,B)) [X1] by H2,
B1';
consider l such that
Line l /\ A IN l /\ B IN l /\ C IN l [X2] by -, Collinear_DEF;
l = m by X1, -, H2, H1, I1;
qed by -, X2`;;
let CollinearLinear_THM = thm `;
let A B C be point;
let m be point_set;
assume Line m /\ A IN m /\ C IN m [H1];
assume Collinear (A,B,C) \/ Collinear (B,C,A) \/ Collinear (C,A,B) [H2];
assume ~(A = C) [H3];
thus B IN m
proof
consider l such that
Line l /\ A IN l /\ B IN l /\ C IN l [X1] by H2, Collinear_DEF;
l = m by H3, -, H1, I1;
qed by -, X1`;;
let NonCollinearImpliesDistinct_THM = thm `;
let A B C be point;
assume ~Collinear (A,B,C) [H1];
thus ~(A = B) /\ ~(A = C) /\ ~(B = C)
proof
cases;
suppose A = B /\ B = C [C1];
consider Q such that ~(Q = A) by OnePointImpliesAnother_THM;
consider l such that Line l /\ A IN l /\ Q IN l by -, I1;
Collinear (A,B,C) by -, C1, Collinear_DEF;
qed by -, H1;
suppose ~(A = B) /\ B = C [C2];
consider l such that Line l /\ A IN l /\ B IN l by -, I1;
Collinear (A,B,C) by -, C2, Collinear_DEF;
qed by -, H1;
suppose ~(B = C) [C3];
consider l such that Line l /\ B IN l /\ C IN l [X1] by C3, I1;
~(A = B) [U]
proof
assume A = B;
Collinear (A,B,C) by -, X1, Collinear_DEF;
qed by -, H1;
~(A = C) [V]
proof
assume A = C;
Collinear (A,B,C) by -, X1, Collinear_DEF;
qed by -, H1;
qed by U, V, C3;
end`;;
let OriginInRay_THM = thm `;
let O Q be point;
assume ~(Q = O) [H1];
thus O IN ray (O,Q)
proof
~(O IN open_int (O,Q)) [OOQ] by B1';
consider l such that
Line l /\ O IN l /\ Q IN l by H1, I1;
Collinear (O,Q,O) by -, Collinear_DEF;
qed by H1, -, OOQ, IN, Ray_DEF`;;
let Line01infinity_THM = thm `;
let X be point;
let l m be point_set;
assume Line l /\ Line m [H0];
assume ~(l = m) [H1];
assume X IN l /\ X IN m [H2];
thus l INTER m = {X}
proof
(l INTER m = {X}) \/ ~(l INTER m = {X});
assume ~(l INTER m = {X}) [H3];
X IN l INTER m by H2, IN_INTER;
consider A such that
A IN l INTER m /\ ~(A = X) [X1] by -, H3, BiggerThanSingleton_THM;
A IN l /\ X IN l /\ A IN m /\ X IN m by H0, -, H2, IN_INTER;
l = m by H0, -, X1, I1;
F by -, H1;
qed by -`;;
let EquivIntersection_THM = thm `;
let A B X be point;
let l m be point_set;
assume Line l /\ Line m [H0];
assume l INTER m = {X} [H1];
assume A IN m DELETE X /\ B IN m DELETE X [H2];
assume ~(X IN open_int (A,B)) [H3];
thus ~(A IN l) /\ ~(B IN l) /\ A,B same_side l
proof
A IN m /\ ~(A = X) [X1] by H2, IN_DELETE;
B IN m /\ ~(B = X) [X2] by H2, IN_DELETE;
~(A IN l) /\ ~(B IN l) [X3] by H1, H2, EquivIntersectionHelp_THM;
A,B same_side l [X4]
proof
assume ~(A,B same_side l);
consider G such that
(G IN l) /\ G IN open_int (A,B) [X5] by H0, -, same_side_DEF;
~(A = B) /\ Collinear (A,G,B) [X6] by -, B1';
consider k such that
Line k /\ A IN k /\ G IN k /\ B IN k [X7] by -, Collinear_DEF;
k = m by H0, -, X1, X2, X6, I1;
G IN l INTER m by -, X5, X7, IN_INTER;
G = X by -, H1, IN_SING;
X IN open_int (A,B) by -, X5;
F by -, H3;
qed by -;
qed by X3, X4`;;
let SameSideReflexiveRelation_THM = thm `;
thus Reflexive_Property
proof
!l A. Line l ==> A,A same_side l
proof
let l be point_set;
let A be point;
assume Line l [H0];
~(?X. (X IN l) /\ X IN open_int (A,A)) by H0, B1';
qed by H0, -, same_side_DEF;
qed by -, Reflexive_relation_DEF`;;
let SameSideSymmetricRelation_THM = thm `;
thus Symmetric_Property
proof
!l A B. Line l /\ ~(A IN l) /\ ~(B IN l) ==>
A,B same_side l ==> B,A same_side l
proof
let l be point_set;
let A B be point;
assume Line l [H0];
assume A,B same_side l [H1];
assume ~(A IN l) /\ ~(B IN l);
~(?X. (X IN l) /\ X IN open_int (A,B)) by H0, H1, same_side_DEF;
~(?X. (X IN l) /\ X IN open_int (B,A)) by -, B1';
qed by H0, -, same_side_DEF;
qed by -, Symmetric_relation_DEF`;;
let SameSideTransitiveRelation_THM = thm `;
thus Transitive_Property
proof
!l A B C.
Line l /\ ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) ==>
A,B same_side l /\ B,C same_side l ==> A,C same_side l
proof
let l be point_set;
let A B C be point;
assume Line l [lLine];
assume ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) [H0];
assume A,B same_side l [H1];
assume B,C same_side l [H2];
A,C same_side l
proof
~Collinear (A,B,C) \/ Collinear (A,B,C);
cases by -;
suppose ~Collinear (A,B,C);
qed by lLine, -, H0, H1, H2, B4'';
suppose Collinear (A,B,C) [Coll];
cases;
suppose A = B \/ A = C \/ B = C;
qed by lLine, -, H2, H0, SameSideReflexiveRelation_THM,
Reflexive_relation_DEF, H1;
suppose ~(A = B) /\ ~(A = C) /\ ~(B = C) [Distinct];
consider m such that
Line m /\ A IN m /\ C IN m [ACm] by Distinct, I1;
~(l = m) [not_lm] by ACm, H0;
cases;
suppose l INTER m = {} [Disjoint];
!X. X IN open_int (A,C) ==> ~(X IN l)
proof
let X be point;
assume X IN open_int (A,C);
X IN m by lLine, -, ACm, BetweenLinear_THM;
~(X IN l) by -, Disjoint, DisjointOneNotOther_THM;
qed by -;
qed by lLine, -, same_side_DEF;
suppose ~(l INTER m = {}) [NotDisjoint];
consider X such that
X IN l INTER m by NotDisjoint, MEMBER_NOT_EMPTY;
X IN l /\ X IN m [Xin_lm] by -, IN_INTER;
l INTER m = {X} [lmX] by lLine, ACm, not_lm, -,
Line01infinity_THM;
consider E such that
E IN l /\ ~(E = X) [Einl_X] by Xin_lm, I2;
~(E IN m) [notEm] by lmX, Einl_X,
IntersectionSingletonOneNotOther_THM;
~(E = B) by Einl_X, H0;
consider B' such that
B IN open_int (E,B') by -, B2';
B IN open_int (B',E) [B'BE] by -, B1';
~(B' = E) /\ ~(B = E) /\ ~(B' = B) /\ Collinear (B',B,E)
[B'BEcol] by -, B1';
consider n such that
Line n /\ E IN n /\ B' IN n [EB'n] by -, I1;
B IN n [Bn] by EB'n, B'BE, BetweenLinear_THM;
~(l = n) [not_ln] by H0, -;
l INTER n = {E} [lnE] by lLine, not_ln, EB'n, Einl_X,
Line01infinity_THM;
~(B' IN l) [notB'l] by -, EB'n, B'BEcol,
IntersectionSingletonOneNotOther_THM;
~(E IN open_int (B,B')) [BEB'] by B'BEcol, B'BE, B3';
B' IN n DELETE E /\ B IN n DELETE E by EB'n, Bn, B'BEcol,
IN_DELETE;
B, B' same_side l [Bsim_lB'] by lLine, EB'n, lnE, -, BEB',
EquivIntersection_THM;
~(m = n) [not_mn] by EB'n, notEm;
B IN m by ACm, Coll, Distinct, CollinearLinear_THM;
m INTER n = {B} [mn_B] by ACm, EB'n, -, Bn, not_mn,
Line01infinity_THM;
~(A IN n) [not_An] by -, ACm, Distinct,
IntersectionSingletonOneNotOther_THM;
~Collinear (A,B,B')
proof
assume Collinear (A,B,B');
consider alpha such that
Line alpha /\ A IN alpha /\ B IN alpha /\ B' IN alpha
[ABB'alpha] by -, Collinear_DEF;
alpha = n by B'BEcol, ABB'alpha, EB'n, Bn, I1;
A IN n by -, ABB'alpha;
qed by -, not_An;
A,B' same_side l [Asim_lB'] by lLine, -, H0, notB'l, H1,
Bsim_lB', B4'';
~(C IN n) [notCn] by mn_B, ACm, Distinct,
IntersectionSingletonOneNotOther_THM;
C,B same_side l [Csim_lB] by lLine, H0, H2,
SameSideSymmetricRelation_THM,
Symmetric_relation_DEF;
~Collinear (C,B,B')
proof
assume Collinear (C,B,B');
consider alpha such that
Line alpha /\ C IN alpha /\ B IN alpha /\ B' IN alpha
[CBB'alpha] by -, Collinear_DEF;
alpha = n by -, EB'n, B'BEcol, CBB'alpha, Bn, I1;
C IN n by -, CBB'alpha;
qed by -, notCn;
C,B' same_side l by lLine, -, H0, notB'l, Csim_lB, Bsim_lB', B4'';
B',C same_side l [B'sim_C] by lLine, H0, notB'l, -,
SameSideSymmetricRelation_THM,
Symmetric_relation_DEF;
~(B' IN m) [notB'm] by mn_B, EB'n, B'BEcol,
IntersectionSingletonOneNotOther_THM;
~Collinear (A,B',C)
proof
assume Collinear (A,B',C);
consider alpha such that
Line alpha /\ A IN alpha /\ B' IN alpha /\ C IN alpha
[AB'Calpha] by -, Collinear_DEF;
alpha = m by Distinct, -, ACm, I1;
B' IN m by -, AB'Calpha;
F by -, notB'm;
qed by -;
A, C same_side l by lLine, -, H0, notB'l, Asim_lB', B'sim_C, B4'';
qed by -;
end;
end;
end;
qed by -;
qed by -, Transitive_relation_DEF`;;
let SameSideEquivalenceRelation_THM = thm `;
thus Reflexive_Property /\ Symmetric_Property /\ Transitive_Property
proof
qed by SameSideReflexiveRelation_THM, SameSideSymmetricRelation_THM,
SameSideTransitiveRelation_THM`;;
let ConverseCrossbar_THM = thm `;
let O A B G be point;
assume ~Collinear (A,O,B) [H1];
assume G IN open_int (A,B) [H2];
thus G int_angle A,O,B
proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1,
NonCollinearImpliesDistinct_THM;
consider a such that Line a /\ O IN a /\ A IN a
[aOA] by -, I1;
consider b such that Line b /\ O IN b /\ B IN b [bOB] by
Distinct, I1;
consider l such that Line l /\ A IN l /\ B IN l [lAB] by
Distinct, I1;
~(B IN a) by H1, aOA, Collinear_DEF;
~(a = l) by -, lAB;
a INTER l = {A} [alA] by -, aOA, lAB,
Line01infinity_THM;
~(A = G) /\ ~(A = B) /\ ~(G = B) /\ G IN open_int (B,A) /\ Collinear
(A,G,B)
[X1] by H2,
B1';
~(A IN open_int (G,B)) [notGAB] by -, H2,
B3', B1';
G IN l [Ginl] by lAB, H2,
BetweenLinear_THM;
~(G IN a) [notGina] by alA, Ginl, X1,
IntersectionSingletonOneNotOther_THM;
G IN l DELETE A /\ B IN l DELETE A by Ginl, lAB, X1, IN_DELETE;
G,B same_side a [Gsim_aB] by aOA, lAB, alA, -, notGAB,
EquivIntersection_THM;
:: same argument shows G,A same_side b
~(A IN b) by H1, bOB, Collinear_DEF;
~(b = l) by -, lAB;
b INTER l = {B} [blB] by -, bOB, lAB,
Line01infinity_THM;
~(B IN open_int (G,A)) [notGBA] by H2, B1', B3';
~(G IN b) [notGinb] by blB, Ginl, X1,
IntersectionSingletonOneNotOther_THM;
G IN l DELETE B /\ A IN l DELETE B by Ginl, lAB, X1, IN_DELETE;
G,A same_side b [Gsim_bA] by bOB, lAB, blB, -, notGBA,
EquivIntersection_THM;
qed by H1, aOA, bOB, notGina, notGinb, Gsim_aB, Gsim_bA, InteriorAngle_DEF`;;
let InteriorHelp_THM = thm `;
let A O B P be point;
let a b be point_set;
assume Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b
[aOAbOB];
assume P int_angle A,O,B [P_AOB];
thus ~(P IN a) /\ ~(P IN b) /\ P,B same_side a /\ P,A same_side b
proof
consider alpha beta such that ~Collinear (A,O,B) /\
Line alpha /\ O IN alpha /\ A IN alpha /\
Line beta /\ O IN beta /\B IN beta /\
~(P IN alpha) /\ ~(P IN beta) /\
P,B same_side alpha /\ P,A same_side beta [exists] by P_AOB,
InteriorAngle_DEF;
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by -,
NonCollinearImpliesDistinct_THM;
alpha = a /\ beta = b by -, aOAbOB, exists, I1;
qed by -, exists`;;
let WholeRayInterior_THM = thm `;
let A O B X P be point;
assume ~Collinear (A,O,B) [H1];
assume X int_angle A,O,B [H2];
assume P IN ray (O,X) [H3];
assume ~(P = O) [H4];
thus P int_angle A,O,B
proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1,
NonCollinearImpliesDistinct_THM;
consider a such that Line a /\ O IN a /\ A IN a [a_OA] by Distinct,
I1;
consider b such that Line b /\ O IN b /\ B IN b [b_OB] by Distinct,
I1;
~(X IN a) /\ ~(X IN b) /\ X,B same_side a /\ X,A same_side b [XintAOB] by
H2, a_OA, b_OB, InteriorHelp_THM;
~(O = X) /\ Collinear (O,X,P) /\ ~(O IN open_int (P,X)) [P_OX] by H3, IN,
Ray_DEF;
consider x such that Line x /\ O IN x /\ X IN x [x_OX] by P_OX, I1;
:: P IN x [Pin_x] by x_OX, P_OX, Collinear_DEF, CollinearLinear_THM;
P IN x [Pin_x] by x_OX, P_OX, CollinearLinear_THM;
P IN x DELETE O [Pin_x_O] by Pin_x, H4, IN_DELETE;
X IN x DELETE O [Xin_x_O] by x_OX, P_OX, IN_DELETE;
~(x = a) /\ ~(x = b) [x_not_ab] by XintAOB, x_OX;
a INTER x = {O} /\ b INTER x = {O} [axb_intO] by x_not_ab, x_OX, a_OA,
b_OB, Line01infinity_THM;
~(P IN a) /\ P,X same_side a [Psim_aX] by a_OA, x_OX, axb_intO, Pin_x_O,
Xin_x_O, P_OX, EquivIntersection_THM;
~(P IN b) /\ P,X same_side b [Psim_bX] by b_OB, x_OX, axb_intO, Pin_x_O,
Xin_x_O, P_OX, EquivIntersection_THM;
P,B same_side a /\ P,A same_side b by Psim_aX, Psim_bX, XintAOB, a_OA,
b_OB, H1, Collinear_DEF, SameSideTransitiveRelation_THM,
Transitive_relation_DEF;
qed by H1, a_OA, b_OB, Psim_aX, Psim_bX, -, InteriorAngle_DEF`;;
let AngleOrdering_THM = thm `;
let O A P Q be point;
let a be point_set;
assume ~(O = A) [H1];
assume Line a /\ O IN a /\ A IN a
[H2];
assume ~(P IN a) /\ ~(Q IN a) [H3];
assume P, Q same_side a [H4];
assume ~Collinear (P,O,Q) [H5];
thus P int_angle Q,O,A \/ Q int_angle P,O,A
proof
~(P = O) /\ ~(P = Q) /\ ~(O = Q) [Distinct] by H5,
NonCollinearImpliesDistinct_THM;
consider p such that Line p /\ O IN p /\ P IN p [p_OP] by
Distinct, I1;
consider q such that Line q /\ O IN q /\ Q IN q [q_OQ] by
Distinct, I1;
~(q = a) by H3, q_OQ;
q INTER a = {O} by -, H2, q_OQ, Line01infinity_THM;
~(A IN q) by -, H2, H1, IntersectionSingletonOneNotOther_THM;
~(P IN q) [notPq] by q_OQ, H5, Collinear_DEF;
~(p = q) by -, p_OP;
p INTER q = {O} by -, p_OP, q_OQ, Line01infinity_THM;
~Collinear (Q,O,A) [QOA_noncol] by H1, H2, I1, H3, Collinear_DEF;
~Collinear (P,O,A) [POA_noncol] by H1, H2, I1, H3, Collinear_DEF;
assume ~(P int_angle Q,O,A) [notP_QOA];
Q int_angle P,O,A
proof
~(P,A same_side q) by QOA_noncol, H2, q_OQ, H3,
notPq, H4, notP_QOA, InteriorAngle_DEF;
consider G such that (G IN q) /\ G IN open_int (P,A) [existG] by q_OQ, -,
same_side_DEF;
G int_angle P,O,A [G_POA] by POA_noncol, existG, ConverseCrossbar_THM;
~(G IN a) /\ G,P same_side a [Gsim_aP] by -, InteriorAngle_DEF, H1, H2,
I1;
~(G = O) [GnotO] by -, H2;
G,Q same_side a by H2, Gsim_aP, H3, H4,
SameSideTransitiveRelation_THM, Transitive_relation_DEF;
~(O IN open_int (Q,G)) [notQOG] by -, same_side_DEF, H2, B1';
Collinear (O,G,Q) by q_OQ, existG, Collinear_DEF;
Q IN ray (O,G) by GnotO, -, notQOG, IN, Ray_DEF;
qed by POA_noncol, G_POA, -, Distinct, WholeRayInterior_THM;
qed by -`;;
let InteriorReflectionInterior_THM = thm `;
let A O B D A' be point;
assume ~Collinear (A,O,B) [H1];
assume D int_angle A,O,B [H2];
assume O IN open_int (A,A') [H3];
thus B int_angle D,O,A'
proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1,
NonCollinearImpliesDistinct_THM;
consider a such that
Line a /\ O IN a /\ A IN a [a_OA] by
Distinct, I1;
consider b such that
Line b /\ O IN b /\ B IN b [b_OB] by
Distinct, I1;
~(A IN b) [notAb] by b_OB, H1, Collinear_DEF;
~(B IN a) [notBa] by a_OA, H1, Collinear_DEF;
~(a = b) by -, b_OB;
b INTER a = {O} [ab_O] by -, a_OA, b_OB, Line01infinity_THM;
A' IN a [A'a] by H3, a_OA, BetweenLinear_THM;
A' IN a DELETE O by A'a, H3, B1', IN_DELETE;
~(A' IN b) [notA'b] by ab_O, -, EquivIntersectionHelp_THM;
~(A,A' same_side b) [Ansim_bA'] by b_OB, H3, same_side_DEF ;
~(D IN a) /\ ~(D IN b) /\
D,B same_side a /\ D,A same_side b [DintAOB] by a_OA, b_OB, H2,
InteriorHelp_THM;
~(D,A' same_side b) [Dnsim_bA']
proof
assume D,A' same_side b;
A',D same_side b by b_OB, DintAOB, notA'b, -,
SameSideSymmetricRelation_THM, Symmetric_relation_DEF;
A',A same_side b by b_OB, DintAOB, notA'b, notAb, -,
SameSideTransitiveRelation_THM, Transitive_relation_DEF;
A,A' same_side b by b_OB, notA'b, notAb, -,
SameSideSymmetricRelation_THM, Symmetric_relation_DEF;
F by -, Ansim_bA';
qed by -;
~(D int_angle B,O,A') [notD_BOA']
proof
assume D int_angle B,O,A';
D,A' same_side b by b_OB, a_OA, A'a, -, DintAOB, InteriorHelp_THM;
F by -, Dnsim_bA';
qed by -;
~Collinear (D,O,B) [DOB_noncol] by Distinct, b_OB, I1, DintAOB,
Collinear_DEF;
~(O = A') by H3, B1';
B int_angle D,O,A' by -, a_OA, A'a, DintAOB, notBa, DOB_noncol, notD_BOA',
AngleOrdering_THM;
qed by -`;;
let Crossbar_THM = thm `;
let O A B D be point;
assume ~Collinear (A,O,B) [H1];
assume D int_angle A,O,B [H2];
thus ?G. G IN open_int (A,B) /\ G IN ray (O,D)
proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1,
NonCollinearImpliesDistinct_THM;
consider a such that
Line a /\ O IN a /\ A IN a [a_OA] by
Distinct, I1;
consider b such that
Line b /\ O IN b /\ B IN b [b_OB] by
Distinct, I1;
~(B IN a) [notBa] by a_OA, H1, Collinear_DEF;
~(D IN a) /\ ~(D IN b) /\ D,B same_side a [D_AOB] by a_OA, b_OB, H2,
InteriorHelp_THM;
~(D = O) [DnotO] by D_AOB, a_OA;
consider l such that
Line l /\ O IN l /\ D IN l [l_OD] by -, I1;
~(a = l) /\ ~(b = l) [abl_distinct] by l_OD, D_AOB, b_OB, notBa;
a INTER l = {O} [alO] by abl_distinct, a_OA, l_OD, Line01infinity_THM;
b INTER l = {O} [blO] by abl_distinct, b_OB, l_OD, Line01infinity_THM;
~(A IN l) /\ ~(B IN l) [ABnot_l] by alO, blO, a_OA, b_OB, Distinct,
IntersectionSingletonOneNotOther_THM;
consider A' such that O IN open_int (A,A') [AOA'] by Distinct,
B2';
A' IN a [A'a] by a_OA, -, BetweenLinear_THM;
~(A' = O) [A'notO] by AOA', B1';
~(A,A' same_side l) [Ansim_lA'] by l_OD, AOA', same_side_DEF;
~(A' IN l) [A'not_l] by alO, A'a, A'notO,
IntersectionSingletonOneNotOther_THM;
B int_angle D,O,A' by H1, H2, AOA', InteriorReflectionInterior_THM;
B,A' same_side l [Bsim_lA'] by l_OD, a_OA, A'a, -, InteriorHelp_THM;
~(A,B same_side l) [Ansim_lB]
proof
assume A,B same_side l;
A,A' same_side l by l_OD, ABnot_l, A'not_l, -, Bsim_lA',
SameSideTransitiveRelation_THM, Transitive_relation_DEF;
qed by -, Ansim_lA';
consider G such that
G IN open_int (A,B) /\ G IN l [AGB] by l_OD, Ansim_lB,
same_side_DEF;
Collinear (O,D,G) [ODGcol] by AGB, l_OD, Collinear_DEF;
G int_angle A,O,B by H1, AGB, ConverseCrossbar_THM;
~(G IN a) /\ G,B same_side a [Gsim_aB] by a_OA, b_OB, -, InteriorHelp_THM;
D,B same_side a by a_OA, b_OB, H2, InteriorHelp_THM;
B,D same_side a by a_OA, notBa, D_AOB, -, SameSideSymmetricRelation_THM,
Symmetric_relation_DEF;
G,D same_side a [Gsim_aD] by a_OA, Gsim_aB, notBa, D_AOB, Gsim_aB, -,
SameSideTransitiveRelation_THM, Transitive_relation_DEF;
~(O IN open_int (G,D)) by a_OA, -, same_side_DEF;
G IN ray (O,D) [G_OD] by DnotO, ODGcol, -, IN, Ray_DEF;
qed by AGB, G_OD`;;
let IntervalTransitivity_THM = thm `;
let O P Q R be point;
let m be point_set;
assume Line m [H0];
assume O IN m [H1];
assume P IN m DELETE O /\ Q IN m DELETE O /\ R IN m DELETE O [H2];
assume ~(O IN open_int (P,Q)) /\ ~(O IN open_int (Q,R)) [H3];
thus ~(O IN open_int (P,R))
proof
P IN m /\ Q IN m /\ R IN m /\ ~(P = O) /\ ~(Q = O) /\ ~(R = O) [H2'] by H2,
IN_DELETE;
consider E such that
~(E IN m) [notEm] by H0, ExistsPointOffLine_THM;
~(O = E) by H1, notEm;
consider l such that
Line l /\ O IN l /\ E IN l [OE_l] by -, I1;
~(m = l) by notEm, OE_l;
l INTER m = {O} [ml_O] by OE_l, H0, -, H1, OE_l,
Line01infinity_THM;
~(P IN l) /\ ~(Q IN l) /\ ~(R IN l) [PQRnotl] by ml_O, H2',
IntersectionSingletonOneNotOther_THM;
P,Q same_side l /\ Q,R same_side l [Psim_lQsim_lR] by OE_l, H0, ml_O, H2,
H3, PQRnotl, EquivIntersection_THM;
P,R same_side l [Psim_lR] by OE_l, PQRnotl,
Psim_lQsim_lR,
SameSideTransitiveRelation_THM,
Transitive_relation_DEF;
qed by OE_l, -, same_side_DEF`;;
let RayLine_THM = thm `;
let O P X be point;
let l be point_set;
assume Line l /\ O IN l /\ P IN l [H1];
assume X IN ray (O,P) [H2];
thus X IN l
proof
~(O = P) /\ Collinear (O,P,X) by H2, IN, Ray_DEF;
X IN l by H1, -, CollinearLinear_THM;
qed by -`;;
let RayWellDefinedHalfway_THM = thm `;
let O P Q be point;
assume ~(Q = O) [H1];
assume P IN ray (O,Q) DELETE O [H2];
thus ray (O,P) SUBSET ray (O,Q)
proof
consider m such that
Line m /\ O IN m /\ Q IN m [OQm] by H1, I1;
P IN ray (O,Q) /\ ~(P = O) [H2'] by H2, IN_DELETE;
P IN m [Pm] by OQm, H2', RayLine_THM;
P IN m DELETE O /\ Q IN m DELETE O [PQm_O] by Pm, H2', OQm, H1, IN_DELETE;
~(O IN open_int (P,Q)) [notPOQ] by H2', IN, Ray_DEF;
!X. X IN ray (O,P) ==> X IN ray (O,Q)
proof
let X be point;
assume X IN ray (O,P) [XrOP];
X IN m [Xm] by OQm, Pm, H2', -, RayLine_THM;
Collinear (O,Q,X) [OQXcol] by OQm, Xm, Collinear_DEF;
~(O IN open_int (X,P)) [notXOP] by XrOP, IN, Ray_DEF;
cases;
suppose X = O;
X IN ray (O,Q) by H1, -, OriginInRay_THM;
qed by -;
suppose ~(X = O) [notXO];
X IN m DELETE O by Xm, notXO, IN_DELETE;
~(O IN open_int (X,Q)) by OQm, -, PQm_O, notXOP, notPOQ,
IntervalTransitivity_THM;
X IN ray (O,Q) by H1, OQXcol, -, IN, Ray_DEF;
qed by -;
end;
qed by -, SUBSET`;;
let RayWellDefined_THM = thm `;
let O P Q be point;
assume ~(Q = O) [H1];
assume P IN ray (O,Q) DELETE O [H2];
thus ray (O,P) = ray (O,Q)
proof
ray (O,P) SUBSET ray (O,Q) [PsubsetQ] by H1, H2,
RayWellDefinedHalfway_THM;
P IN ray (O,Q) /\ ~(P = O) [H2'] by H2, IN_DELETE;
Collinear (O,Q,P) /\ ~(O IN open_int (P,Q)) [notPOQ] by H2', IN,
Ray_DEF;
Collinear (O,P,Q) [OQPcol] by notPOQ, CollinearSymmetry_THM;
~(O IN open_int (Q,P)) [notQOP] by notPOQ, B1';
Q IN ray (O,P) by H2', OQPcol, notQOP, IN, Ray_DEF;
Q IN ray (O,P) DELETE O [QrOP_O] by -, H1, IN_DELETE;
ray (O,Q) SUBSET ray (O,P) [QsubsetP] by H2', QrOP_O,
RayWellDefinedHalfway_THM;
qed by PsubsetQ, QsubsetP, DoubleSubsetEqual_THM `;;
let OppositeRaysIntersect1pointHelp_THM = thm `;
let A O B X be point;
assume O IN open_int (A,B)
[H1];
assume X IN ray (O,B) DELETE O [H2];
thus ~(X IN ray (O,A))
proof
~(A = O) /\ ~(A = B) /\ ~(O = B) /\ Collinear (A,O,B) [B1_AOB] by H1, B1';
X IN ray (O,B) /\ ~(X = O) [H2'] by H2, IN_DELETE;
Collinear (O,B,X) /\ ~(O IN open_int (X,B)) [K2] by -, IN, Ray_DEF;
consider m such that
Line m /\ A IN m /\ B IN m [ABm] by B1_AOB, I1;
O IN m [Om] by ABm, B1_AOB, CollinearLinear_THM;
X IN m [Xm] by ABm, Om, K2, B1_AOB, CollinearLinear_THM;
A IN m DELETE O /\ X IN m DELETE O /\ B IN m DELETE O [AXBm_O] by ABm,
Xm, H2', B1_AOB, IN_DELETE;
O IN open_int (A,X) by H1, ABm, Om, AXBm_O, K2, IntervalTransitivity_THM;
O IN open_int (X,A) by -, B1';
qed by -, IN, Ray_DEF`;;
let OppositeRaysIntersect1point_THM = thm `;
let A O B be point;
assume O IN open_int (A,B)
[H1];
thus ray (O,A) INTER ray (O,B) = {O}
proof
~(A = O) /\ ~(A = B) /\ ~(O = B) /\ O IN open_int (B,A) /\ Collinear
(A,O,B) [B1_AOB] by H1, B1';
O IN ray (O,A) INTER ray (O,B) by B1_AOB, OriginInRay_THM, IN_INTER;
{O} SUBSET ray (O,A) INTER ray (O,B) [Osubset_rOA] by -, SING_SUBSET;
ray (O,A) INTER ray (O,B) SUBSET {O}
proof
!X. X IN ray (O,A) INTER ray (O,B) ==> X IN {O}
proof
let X be point;
assume X IN ray (O,A) INTER ray (O,B);
X IN ray (O,A) /\ X IN ray (O,B) [XinBothRays] by -, IN_INTER;
cases;
suppose X = O;
qed by -, IN_SING;
suppose ~(X = O);
X IN ray (O,B) DELETE O by -, XinBothRays, IN_DELETE;
~(X IN ray (O,A)) by H1, -, OppositeRaysIntersect1pointHelp_THM;
F by -, XinBothRays;
qed by -;
end;
qed by -, SUBSET;
qed by -, Osubset_rOA, DoubleSubsetEqual_THM`;;
let TransitivitybetweennessHelp_THM = thm `;
let A B C D be point;
assume B IN open_int (A,C) /\ C IN open_int (B,D) [H1];
thus B IN open_int (A,D)
proof
~(A = B) /\ ~(A = C) /\ ~(B = C) [Distinct] by H1, B1';
consider l such that
Line l /\ A IN l /\ C IN l [ACl] by Distinct, I1;
B IN l /\ D IN l by ACl, H1, BetweenLinear_THM;
Collinear (B,A,D) [BADcol] by ACl, -, Collinear_DEF;
~(B IN open_int (D,C)) by H1, B1', B3';
D IN ray (B,C) DELETE B by Distinct, H1, B1', -, IN, Ray_DEF, IN_DELETE;
~(D IN ray (B,A)) by Distinct, H1, -, OppositeRaysIntersect1pointHelp_THM;
B IN open_int (D,A) by Distinct, BADcol, -, IN, Ray_DEF;
qed by -, B1'`;;
let Transitivitybetweenness_THM = thm `;
let A B C D be point;
assume B IN open_int (A,C) /\ C IN open_int (B,D) [H1];
thus is_ordered (A,B,C,D)
proof
B IN open_int (A,D) [ABD] by H1, TransitivitybetweennessHelp_THM;
C IN open_int (D,B) /\ B IN open_int (C,A) by H1, B1';
C IN open_int (D,A) [DCA] by -, TransitivitybetweennessHelp_THM;
C IN open_int (A,D) by -, B1';
qed by H1, ABD, -, is_ordered_DEF`;;
let Transitivitybetweenness_THM = thm `;
let A B C D be point;
assume B IN open_int (A,C) /\ C IN open_int (B,D) [H1];
thus is_ordered (A,B,C,D)
proof
!P Q R S. Q IN open_int (P,R) /\ R IN open_int (Q,S) ==> Q IN open_int
(P,S) [help]
proof
let P Q R S be point;
assume Q IN open_int (P,R) /\ R IN open_int (Q,S) [PQRS];
~(P = Q) /\ ~(P = R) /\ ~(Q = R) [Distinct] by PQRS, B1';
consider l such that
Line l /\ P IN l /\ R IN l [PRl] by Distinct, I1;
Q IN l /\ S IN l by PRl, PQRS, BetweenLinear_THM;
Collinear (Q,P,S) [QPScol] by PRl, -, Collinear_DEF;
~(Q IN open_int (S,R)) by PQRS, B1', B3';
S IN ray (Q,R) DELETE Q by Distinct, PQRS, B1', -, IN, Ray_DEF,
IN_DELETE;
~(S IN ray (Q,P)) by Distinct, PQRS, -,
OppositeRaysIntersect1pointHelp_THM;
Q IN open_int (S,P) by Distinct, QPScol, -, IN, Ray_DEF;
qed by -, B1';
B IN open_int (A,D) [ABD] by H1, help;
C IN open_int (D,B) /\ B IN open_int (C,A) by H1, B1';
C IN open_int (D,A) [DCA] by -, help;
C IN open_int (A,D) by -, B1';
qed by H1, ABD, -, is_ordered_DEF`;;
let IntervalsAreConvex_THM = thm `;
let A B C be point;
assume B IN open_int (A,C) [H1];
thus open_int (A,B) SUBSET open_int (A,C)
proof
!X. X IN open_int (A,B) ==> X IN open_int (A,C)
proof
let X be point;
assume X IN open_int (A,B) [XinAB];
~(A = X) /\ ~(A = B) /\ ~(A = C) /\ ~(X = B) /\ ~(B = C) [Distinct] by
H1, XinAB, B1';
consider l such that
Line l /\ A IN l /\ C IN l [ACl] by Distinct, I1;
B IN l /\ X IN l by ACl, H1, XinAB, B1', BetweenLinear_THM;
Collinear (B,C,X) [BCXcol] by ACl, -, Collinear_DEF;
Collinear (B,A,X) [ABXcol] by XinAB, B1', CollinearSymmetry_THM ;
~(B IN open_int (X,A)) by Distinct, ABXcol, XinAB, B3';
X IN ray (B,A) DELETE B [XrBA_B] by Distinct, ABXcol, -, Ray_DEF, IN,
IN_DELETE;
~(X IN ray (B,C)) [notXrBC] by H1, B1', XrBA_B,
OppositeRaysIntersect1pointHelp_THM;
B IN open_int (X,C) by Distinct, BCXcol, notXrBC, IN, Ray_DEF;
X IN open_int (A,C) by XinAB, -, TransitivitybetweennessHelp_THM;
qed by -;
qed by -, SUBSET`;;
let TransitivityBetweennessVariant_THM = thm `;
let A X B C be point;
assume X IN open_int (A,B) /\ B IN open_int (A,C) [H1];
thus is_ordered (A,X,B,C)
proof
~(A = X) /\ ~(A = B) /\ ~(A = C) /\ ~(X = B) /\ ~(B = C) [Distinct] by
H1, B1';
consider l such that
Line l /\ A IN l /\ C IN l [ACl] by Distinct, I1;
B IN l /\ X IN l by ACl, H1, B1', BetweenLinear_THM;
Collinear (B,C,X) [BCXcol] by H1, ACl, -, Collinear_DEF;
Collinear (B,A,X) [ABXcol] by H1, B1', CollinearSymmetry_THM ;
~(B IN open_int (X,A)) by Distinct, ABXcol, H1, B3';
X IN ray (B,A) DELETE B [XrBA_B] by Distinct, ABXcol, -, Ray_DEF, IN,
IN_DELETE;
~(X IN ray (B,C)) [notXrBC] by H1, B1', XrBA_B,
OppositeRaysIntersect1pointHelp_THM;
B IN open_int (X,C) by Distinct, BCXcol, notXrBC, IN, Ray_DEF;
is_ordered (A,X,B,C) by H1, -, Transitivitybetweenness_THM;
qed by -`;;
let Interval2sides2aLineHelp_THM = thm `;
let A B C X be point;
let l be point_set;
assume ~(A = B) /\ ~(A = C) /\ ~(A = X) /\ ~(B = C) /\ ~(B = X) /\ ~(C = X)
[H1];
assume Line l /\ A IN l /\ B IN l /\ C IN l /\ X IN l [H2];
assume B IN open_int (A,C) [H3];
thus ~(X IN open_int (A,B)) \/ ~(X IN open_int (B,C))
proof
assume X IN open_int (A,B) [X_AB];
Collinear (X,B,C) [XBCcol] by H2, Collinear_DEF;
is_ordered (A,X,B,C) [AXBC] by X_AB, H3,
TransitivityBetweennessVariant_THM;
B IN open_int (X,C) [B_XC] by AXBC, is_ordered_DEF;
~(X IN open_int (C,B)) by H1, XBCcol, B_XC, B3';
qed by -, B1'`;;
let Interval2sides2aLine_THM = thm `;
let A B C X be point;
let l be point_set;
assume ~(A = B) /\ ~(A = C) /\ ~(A = X) /\ ~(B = C) /\ ~(B = X) /\ ~(C = X)
[H1];
assume Line l /\ A IN l /\ B IN l /\ C IN l /\ X IN l [H2];
thus ~(X IN open_int (A,B)) \/ ~(X IN open_int (B,C)) \/ ~(X IN open_int
(A,C))
proof
Collinear (A,B,C) by H2, Collinear_DEF;
B IN open_int (A,C) \/ C IN open_int (B,A) \/ A IN open_int (C,B) by H1, -,
B3';
cases by -;
suppose B IN open_int (A,C);
qed by H1, H2, -, Interval2sides2aLineHelp_THM;
suppose C IN open_int (B,A);
~(X IN open_int (B,C)) \/ ~(X IN open_int (C,A)) by H1, H2, -,
Interval2sides2aLineHelp_THM;
qed by -, B1';
suppose A IN open_int (C,B);
~(X IN open_int (C,A)) \/ ~(X IN open_int (A,B)) by H1, H2, -,
Interval2sides2aLineHelp_THM;
qed by -, B1';
end`;;
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
