:: Semi-Affine Space
:: by Eugeniusz Kusak and Krzysztof Radziszewski
::
:: Received November 30, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ANALOAF, SUBSET_1, DIRAF, PARSP_2, FDIFF_1, SEMI_AF1,
PENCIL_1;
notations STRUCT_0, ANALOAF, DIRAF;
constructors DIRAF;
registrations ANALOAF, STRUCT_0;
theorems PARDEPAP, DIRAF;
begin
definition
let IT be non empty AffinStruct;
attr IT is Semi_Affine_Space-like means
:Def1:
(for a,b being Element of IT holds a,b // b,a) &
(for a,b,c being Element of IT holds a,b // c,c) &
(for a,b,p,q,r,s being Element of IT holds
( a<>b & a,b // p,q & a,b // r,s implies p,q // r,s )) &
(for a,b,c being Element of IT holds ( a,b // a,c implies b,a // b,c )) &
(ex a,b,c being Element of IT st not a,b // a,c) &
(for a,b,p being Element of IT
ex q being Element of IT st ( a,b // p,q & a,p // b,q )) &
(for o,a being Element of IT holds
(ex p being Element of IT st
(for b,c being Element of IT holds o,a // o,p &
(ex d being Element of IT st
( o,p // o,b implies o,c // o,d & p,c // b,d ))))) &
(for o,a,a9,b,b9,c,c9 being Element of IT holds
( not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c //
o,c9 & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )) &
(for a,a9,b,b9,c,c9 being Element of IT holds
( not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 &
a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )) &
(for a1,a2,a3,b1,b2,b3 being Element of IT holds
( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2
implies a3,b1 // a1,b3 )) &
for a,b,c,d being Element of IT holds
( not a,b // a,c & a,b // c,d & a,c // b,d implies not a,d // b,c );
end;
registration
cluster Semi_Affine_Space-like for non empty AffinStruct;
existence
proof
consider SAS being AffinPlane such that
A1: ( ( for o,a,a9,b,b9,c,c9 being Element of SAS holds ( not o,a // o
,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 &
a,c // a9,c9 implies b,c // b9,c9 ))& for a,a9,b,b9,c,c9 being Element of SAS
holds ( not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b
// a9,b9 & a,c // a9,c9 implies b,c // b9,c9 ) )&( ( for a1,a2,a3,b1,b2,b3
being Element of SAS holds ( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 &
a2,b3 // a3,b2 implies a3,b1 // a1,b3 ))& for a,b,c,d being Element of SAS
holds ( not a,b // a,c & a,b // c,d & a,c // b,d implies not a,d // b,c ) ) by
PARDEPAP:4;
reconsider AS=SAS as non empty AffinStruct;
take AS;
thus for a,b being Element of AS holds a,b // b,a by DIRAF:40;
thus thesis by A1,DIRAF:40,PARDEPAP:5;
end;
end;
definition
mode Semi_Affine_Space is Semi_Affine_Space-like non empty AffinStruct;
end;
::
:: AXIOMS OF SEMI_AFFINE SPACE
::
reserve SAS for Semi_Affine_Space;
reserve a,a9,a1,a2,a3,a4,b,b9,c,c9,d,d9,d1,d2,o,p,p1,p2,q,r,r1,r2,s,x, y,t,z
for Element of SAS;
theorem Th1:
a,b // a,b
proof
b,a // b,b by Def1;
hence thesis by Def1;
end;
theorem Th2:
a,b // c,d implies c,d // a,b
proof
assume
A1: a,b // c,d;
a,b // a,b by Th1;
then a<>b implies c,d // a,b by A1,Def1;
hence thesis by Def1;
end;
theorem Th3:
a,a // b,c
proof
b,c // a,a by Def1;
hence thesis by Th2;
end;
theorem Th4:
a,b // c,d implies b,a // c,d
proof
assume
A1: a,b // c,d;
a,b // b,a by Def1;
then a<>b implies b,a // c,d by A1,Def1;
hence thesis by A1;
end;
theorem Th5:
a,b // c,d implies a,b // d,c
proof
assume a,b // c,d;
then c,d // a,b by Th2;
then d,c // a,b by Th4;
hence thesis by Th2;
end;
theorem Th6:
a,b // c,d implies b,a // c,d & a,b // d,c & b,a // d,c & c,d //
a,b & d,c // a,b & c,d // b,a & d,c // b,a
proof
assume a,b // c,d;
then c,d // a,b by Th2;
then
A1: d,c // a,b by Th4;
then
A2: d,c // b,a by Th5;
then c,d // b,a by Th4;
hence thesis by A1,A2,Th2,Th4;
end;
theorem Th7:
a,b // a,c implies a,c // a,b & b,a // a,c & a,b // c,a & a,c //
b,a & b,a // c,a & c,a // a,b & c,a // b,a & b,a // b,c & a,b // b,c & b,a // c
,b & b,c // b,a & a,b // c,b & c,b // b,a & b,c // a,b & c,b // a,b & c,a // c,
b & a,c // c,b & c,a // b,c & a,c // b,c & c,b // c,a & b,c // c,a & c,b // a,c
& b,c // a,c
proof
assume
A1: a,b // a,c;
then a,c // a,b by Th2;
then
A2: c,a // c,b by Def1;
b,a // b,c by A1,Def1;
hence thesis by A1,A2,Th6;
end;
theorem Th8:
a<>b & p,q // a,b & a,b // r,s implies p,q // r,s
proof
assume that
A1: a<>b and
A2: p,q // a,b and
A3: a,b // r,s;
a,b // p,q by A2,Th6;
hence thesis by A1,A3,Def1;
end;
theorem
not a,b // a,d implies a<>b & b<>d & d<>a by Def1,Th1,Th3;
theorem
not a,b // p,q implies a<>b & p<>q by Def1,Th3;
theorem
a,b // a,x & b,c // b,x & c,a // c,x implies a,b // a,c
proof
assume that
A1: a,b // a,x and
A2: b,c // b,x and
A3: c,a // c,x;
now
assume
A4: a<>x;
a,x // a,b & a,x // a,c by A1,A3,Th7;
hence thesis by A4,Def1;
end;
hence thesis by A2,Th7;
end;
theorem Th12:
not a,b // a,c & p<>q implies not p,q // p,a or not p,q // p,b
or not p,q // p,c
proof
assume that
A1: not a,b // a,c and
A2: p<>q;
now
assume that
A3: a<>p and
A4: p,q // p,a and
A5: p,q // p,b and
A6: p,q // p,c;
p,a // p,c by A2,A4,A6,Def1;
then
A7: a,p // a,c by Def1;
p,a // p,b by A2,A4,A5,Def1;
then a,p // a,b by Def1;
hence contradiction by A1,A3,A7,Def1;
end;
hence thesis by A1,A2,Def1;
end;
theorem Th13:
p<>q implies ex r st not p,q // p,r
proof
consider a,b,c such that
A1: not a,b // a,c by Def1;
assume p<>q;
then not p,q // p,a or not p,q // p,b or not p,q // p,c by A1,Th12;
hence thesis;
end;
theorem Th14:
not a,b // a,c implies not a,b // c,a & not b,a // a,c & not b,a
// c,a & not a,c // a,b & not a,c // b,a & not c,a // a,b & not c,a // b,a &
not b,a // b,c & not b,a // c,b & not a,b // b,c & not a,b // c,b & not b,c //
b,a & not b,c // a,b & not c,b // a,b & not c,b // b,a & not c,b // c,a & not c
,b // a,c & not b,c // c,a & not b,c // a,c & not c,a // c,b & not c,a // b,c &
not a,c // b,c & not a,c // c,b
proof
assume
A1: not a,b // a,c;
A2: now
assume a,c // c,b;
then c,a // c,b by Th6;
hence contradiction by A1,Th7;
end;
assume
A3: not thesis;
not b,a // b,c by A1,Th7;
hence thesis by A1,A3,A2,Th6;
end;
theorem Th15:
not a,b // c,d & a,b // p,q & c,d // r,s & p<>q & r<>s implies not p,q // r,s
proof
assume that
A1: not a,b // c,d and
A2: a,b // p,q and
A3: c,d // r,s and
A4: p<>q and
A5: r<>s;
assume p,q // r,s;
then a,b // r,s by A2,A4,Th8;
then
A6: r,s // a,b by Th6;
r,s // c,d by A3,Th6;
hence contradiction by A1,A5,A6,Def1;
end;
theorem Th16:
not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p<>q
implies not p,q // p,r
proof
assume that
A1: not a,b // a,c and
A2: a,b // p,q and
A3: a,c // p,r and
A4: b,c // q,r and
A5: p<>q;
now
assume p=r;
then
A6: p,q // b,c by A4,Th6;
p,q // a,b by A2,Th6;
then a,b // b,c by A5,A6,Def1;
then b,a // b,c by Th4;
hence contradiction by A1,Th7;
end;
hence thesis by A1,A2,A3,A5,Th15;
end;
theorem Th17:
not a,b // a,c & a,c // p,r & b,c // p,r implies p=r
proof
assume that
A1: ( not a,b // a,c)& a,c // p,r and
A2: b,c // p,r;
A3: p,r // b,c by A2,Th6;
( not a,c // b,c)& p,r // a,c by A1,Th6,Th14;
hence thesis by A3,Def1;
end;
theorem Th18:
not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 implies r1=r2
proof
assume that
A1: ( not p,q // p,r1)& p,r1 // p,r2 and
A2: q,r1 // q,r2;
A3: r1,r2 // r1,q by A2,Th14;
( not r1,p // r1,q)& r1,r2 // r1,p by A1,Th14;
hence thesis by A3,Def1;
end;
theorem Th19:
not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c //
q,r1 & b,c // q,r2 implies r1=r2
proof
assume that
A1: not a,b // a,c and
A2: a,b // p,q and
A3: a,c // p,r1 and
A4: a,c // p,r2 and
A5: b,c // q,r1 and
A6: b,c // q,r2;
A7: now
b<>c by A1,Th1;
then
A8: q,r1 // q,r2 by A5,A6,Def1;
a<>c by A1,Def1;
then
A9: p,r1 // p,r2 by A3,A4,Def1;
assume p<>q;
then not p,q // p,r1 by A1,A2,A3,A5,Th16;
hence thesis by A9,A8,Th18;
end;
now
assume
A10: p=q;
then p=r1 by A1,A3,A5,Th17;
hence thesis by A1,A4,A6,A10,Th17;
end;
hence thesis by A7;
end;
theorem
a=b or c =d or a=c & b=d or a=d & b=c implies a,b // c,d by Def1,Th1,Th3;
theorem
a=b or a=c or b=c implies a,b // a,c by Def1,Th1,Th3;
::
:: BASIC FACTS ABOUT COLLINEARITY RELATION
::
definition
let SAS,a,b,c;
pred a,b,c are_collinear means
a,b // a,c;
end;
theorem Th22:
a1,a2,a3 are_collinear implies a1,a3,a2 are_collinear & a2,a1,a3
are_collinear & a2,a3,a1 are_collinear & a3,a1,a2 are_collinear & a3,a2,a1
are_collinear
by Th7;
theorem Th23:
not a,b,c are_collinear & a,b // p,q & a,c // p,r & p<>q & p<>r
implies not p,q,r are_collinear
by Th15;
theorem Th24:
a=b or b=c or c =a implies a,b,c are_collinear
by Def1,Th1,Th3;
theorem Th25:
p<>q implies ex r st not p,q,r are_collinear
proof
assume p<>q;
then consider r such that
A1: not p,q // p,r by Th13;
take r;
thus thesis by A1;
end;
theorem Th26:
a,b,c are_collinear & a,b,d are_collinear implies a,b // c,d
proof
assume that
A1: a,b,c are_collinear and
A2: a,b,d are_collinear;
now
assume that
A3: a<>b and
A4: a<>c;
A5: a,b // a,c by A1;
a,b // a,d by A2;
then a,c // a,d by A3,A5,Def1;
then a,c // c,d by Th7;
hence thesis by A4,A5,Th8;
end;
hence thesis by A2,Th3;
end;
theorem Th27:
not a,b,c are_collinear & a,b // c,d implies not a,b,d are_collinear
proof
assume that
A1: not a,b,c are_collinear and
A2: a,b // c,d;
now
assume that
A3: c <>d and
A4: a,b,d are_collinear;
a,b // a,d by A4;
then
A5: a,b // d,a by Th6;
A6: a,b // d,c by A2,Th6;
A7: a,c // c,a by Def1;
A8: not a,b // a,c by A1;
then a<>b by Th3;
then
A9: d,c // d,a by A6,A5,Def1;
c <>a by A8,Def1;
then not c,d // c,a by A2,A3,A8,A7,Th15;
hence contradiction by A9,Th7;
end;
hence thesis by A1;
end;
theorem Th28:
not a,b,c are_collinear & a,b // c,d & c <>d & c,d,x are_collinear
implies not a,b,x are_collinear
by Th8,Th27;
theorem
not o,a,b are_collinear & o,a,x are_collinear & o,b,x are_collinear
implies o=x
proof
assume that
A1: not o,a,b are_collinear and
A2: o,a,x are_collinear and
A3: o,b,x are_collinear;
b,o,x are_collinear by A3,Th22;
then
A4: b,o // b,x;
o,a // o,x by A2;
then
A5: a,o // a,x by Th14;
not a,b,o are_collinear by A1,Th22;
then not a,b // a,o;
hence thesis by A5,A4,Th18;
end;
theorem
o<>a & o<>b & o,a,b are_collinear & o,a,a9 are_collinear & o,b,b9
are_collinear implies a,b // a9,b9
proof
assume that
A1: o<>a and
A2: o<>b and
A3: o,a,b are_collinear and
A4: o,a,a9 are_collinear and
A5: o,b, b9 are_collinear;
A6: now
A7: o,a // o,b by A3;
o,a // o,a9 by A4;
then
A8: o,b // o,a9 by A1,A7,Def1;
o,b // o,b9 by A5;
then o,a9 // o,b9 by A2,A8,Def1;
then
A9: o,a9 // a9,b9 by Th7;
o,b // a,b by A7,Th7;
then
A10: a,b // o,a9 by A2,A8,Def1;
assume o<>a9;
hence thesis by A10,A9,Th8;
end;
now
assume
A11: o=a9;
then a9,a // a9,b by A3;
then
A12: a,b // a9,b by Th7;
a9,b // a9,b9 by A5,A11;
hence thesis by A2,A11,A12,Th8;
end;
hence thesis by A6;
end;
theorem
not a,b // c,d & a,b,p1 are_collinear & a,b,p2 are_collinear & c,d,p1
are_collinear & c,d,p2 are_collinear implies p1=p2
proof
assume that
A1: not a,b // c,d and
A2: a,b,p1 are_collinear & a,b,p2 are_collinear and
A3: c,d,p1 are_collinear & c,d,p2 are_collinear;
c,d // p1,p2 by A3,Th26;
then
A4: p1,p2 // c,d by Th6;
a,b // p1,p2 by A2,Th26;
then p1,p2 // a,b by Th6;
hence thesis by A1,A4,Def1;
end;
theorem Th32:
a<>b & a,b,c are_collinear & a,b // c,d implies a,c // b,d
proof
assume that
A1: a<>b and
A2: a,b,c are_collinear and
A3: a,b // c,d;
now
A4: a,b // a,c by A2;
then a,b // c,b by Th7;
then c,b // c,d by A1,A3,Def1;
then
A5: b,c // b,d by Th7;
assume
A6: b<>c;
b,c // a,c by A4,Th7;
hence thesis by A6,A5,Def1;
end;
hence thesis by A3;
end;
theorem Th33:
a<>b & a,b,c are_collinear & a,b // c,d implies c,b // c,d
proof
assume that
A1: a<>b and
A2: a,b,c are_collinear and
A3: a,b // c,d;
now
a,b // a,c by A2;
then
A4: a,c // c,b & a,c // c,d by A1,A3,Def1,Th7;
assume a<>c;
hence thesis by A4,Def1;
end;
hence thesis by A3;
end;
theorem Th34:
not o,a,c are_collinear & o,a,b are_collinear & o,c,d1
are_collinear & o,c,d2 are_collinear & a,c // b,d1 & a,c // b,d2
implies d1=d2
by Th19;
theorem
a<>b & a,b,c are_collinear & a,b,d are_collinear implies a,c,d are_collinear
by Def1;
::
:: PARALLELOGRAM
::
definition
let SAS,a,b,c,d;
pred parallelogram a,b,c,d means
not a,b,c are_collinear & a,b // c,d & a,c // b,d;
end;
theorem Th36:
parallelogram a,b,c,d implies a<>b & a<>c & c <>b & a<>d & b<>d & c <>d
proof
assume
A1: parallelogram a,b,c,d;
then not a,b,c are_collinear;
hence a<>b & a<>c & c <>b by Th24;
A2: now
assume a=d;
then a,b // c,a by A1;
then
A3: a,b // a,c by Th6;
not a,b,c are_collinear by A1;
hence contradiction by A3;
end;
A4: now
assume c =d;
then a,c // b,c by A1;
then c,a // c,b by Th6;
then
A5: c,a,b are_collinear;
not a,b,c are_collinear by A1;
hence contradiction by A5,Th22;
end;
A6: now
assume b=d;
then a,b // c,b by A1;
then b,a // b,c by Th6;
then
A7: b,a,c are_collinear;
not a,b,c are_collinear by A1;
hence contradiction by A7,Th22;
end;
assume not thesis;
hence contradiction by A2,A6,A4;
end;
theorem Th37:
parallelogram a,b,c,d implies not a,b,c are_collinear & not b,a,d
are_collinear & not c,d,a are_collinear & not d,c,b are_collinear
proof
A1: a,b // b,a by Def1;
assume
A2: parallelogram a,b,c,d;
hence not a,b,c are_collinear;
A3: b<>a & b<>d by A2,Th36;
a,c // b,d by A2;
then
A4: a,c // d,b by Th6;
a,b // c,d by A2;
then
A5: a,b // d,c by Th6;
( not a,b,c are_collinear)& a,c // b,d by A2;
hence not b,a,d are_collinear by A1,A3,Th23;
A6: a,c // c,a by Def1;
A7: c <>d & c <>a by A2,Th36;
( not a,b,c are_collinear)& a,b // c,d by A2;
hence not c,d,a are_collinear by A6,A7,Th23;
A8: d<>b by A2,Th36;
( not a,b,c are_collinear)& c <>d by A2,Th36;
hence thesis by A5,A4,A8,Th23;
end;
theorem Th38:
parallelogram a1,a2,a3,a4 implies not a1,a2,a3 are_collinear &
not a1,a3,a2 are_collinear & not a1,a2,a4 are_collinear & not a1,a4,a2
are_collinear & not a1,a3,a4 are_collinear & not a1,a4,a3 are_collinear &
not a2,
a1,a3 are_collinear & not a2,a3,a1 are_collinear &
not a2,a1,a4 are_collinear &
not a2,a4,a1 are_collinear & not a2,a3,a4 are_collinear & not a2,a4,a3
are_collinear & not a3,a1,a2 are_collinear &
not a3,a2,a1 are_collinear & not a3,
a1,a4 are_collinear & not a3,a4,a1 are_collinear &
not a3,a2,a4 are_collinear &
not a3,a4,a2 are_collinear & not a4,a1,a2 are_collinear & not a4,a2,a1
are_collinear & not a4,a1,a3 are_collinear & not a4,a3,a1 are_collinear &
not a4, a2,a3 are_collinear & not a4,a3,a2 are_collinear
proof
assume
A1: parallelogram a1,a2,a3,a4;
then
A2: ( not a3,a4,a1 are_collinear)& not a4,a3,a2 are_collinear by Th37;
( not a1,a2,a3 are_collinear)& not a2,a1,a4 are_collinear by A1,Th37;
hence thesis by A2,Th22;
end;
theorem Th39:
parallelogram a,b,c,d implies not a,b,x are_collinear or not c,d,
x are_collinear
proof
assume
A1: parallelogram a,b,c,d;
then
A2: c <>d by Th36;
( not a,b,c are_collinear)& a,b // c,d by A1;
hence thesis by A2,Th28;
end;
theorem
parallelogram a,b,c,d implies parallelogram a,c,b,d
by Th38;
theorem
parallelogram a,b,c,d implies parallelogram c,d,a,b
by Th6,Th38;
theorem
parallelogram a,b,c,d implies parallelogram b,a,d,c
by Th6,Th38;
theorem Th43:
parallelogram a,b,c,d implies parallelogram a,c,b,d &
parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b &
parallelogram d,b,c,a & parallelogram b,d,a,c
by Th38,Th6;
theorem Th44:
not a,b,c are_collinear implies ex d st parallelogram a,b,c,d
proof
assume
A1: not a,b,c are_collinear;
consider d such that
A2: a,b // c,d & a,c // b,d by Def1;
take d;
thus thesis by A1,A2;
end;
theorem Th45:
parallelogram a,b,c,d1 & parallelogram a,b,c,d2 implies d1=d2
proof
assume that
A1: parallelogram a,b,c,d1 and
A2: parallelogram a,b,c,d2;
not b,c,a are_collinear by A1,Th38;
then
A3: not b,c // b,a;
a,c // b,d2 by A2;
then
A4: c,a // b,d2 by Th6;
a,b // c,d2 by A2;
then
A5: b,a // c,d2 by Th6;
a,c // b,d1 by A1;
then
A6: c,a // b,d1 by Th6;
a,b // c,d1 by A1;
then
A7: b,a // c,d1 by Th6;
b,c // c,b by Def1;
hence thesis by A3,A7,A5,A6,A4,Th19;
end;
theorem Th46:
parallelogram a,b,c,d implies not a,d // b,c
proof
assume
A1: parallelogram a,b,c,d;
then not a,b,c are_collinear;
then
A2: not a,b // a,c;
a,b // c,d & a,c // b,d by A1;
hence thesis by A2,Def1;
end;
theorem Th47:
parallelogram a,b,c,d implies not parallelogram a,b,d,c
proof
assume
A1: parallelogram a,b,c,d;
then not a,b,c are_collinear;
then
A2: not a,b // a,c;
assume not thesis;
then
A3: a,d // b,c;
a,b // c,d & a,c // b,d by A1;
hence contradiction by A3,A2,Def1;
end;
theorem Th48:
a<>b implies ex c st a,b,c are_collinear & c <>a & c <>b
proof
assume a<>b;
then consider p such that
A1: not a,b,p are_collinear by Th25;
consider q such that
A2: parallelogram a,b,p,q by A1,Th44;
not p,q,b are_collinear by A2,Th38;
then consider c such that
A3: parallelogram p,q,b,c by Th44;
take c;
A4: p,q // b,c by A3;
p<>q & a,b // p,q by A2,Th36;
then a,b // b,c by A4,Th8;
then b,a // b,c by Th6;
then
A5: b,a,c are_collinear;
A6: not a,q // b,p by A2,Th46;
p,b // q,c & not b,c,p are_collinear by A3,Th37;
hence thesis by A6,A5,Th6,Th22,Th24;
end;
theorem Th49:
parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 implies b,c // b9,c9
proof
assume that
A1: parallelogram a,a9,b,b9 and
A2: parallelogram a,a9,c,c9;
A3: a,a9 // c,c9 & a,c // a9,c9 by A2;
not a,a9,c are_collinear by A2;
then
A4: not a,a9 // a,c;
not a,a9,b are_collinear by A1;
then
A5: not a,a9 // a,b;
a,a9 // b,b9 & a,b // a9,b9 by A1;
hence thesis by A5,A4,A3,Def1;
end;
theorem Th50:
not b,b9,c are_collinear & parallelogram a,a9,b,b9 &
parallelogram a,a9,c,c9 implies parallelogram b,b9,c,c9
proof
assume that
A1: not b,b9,c are_collinear and
A2: parallelogram a,a9,b,b9 and
A3: parallelogram a,a9,c,c9;
A4: a,a9 // c,c9 by A3;
a<>a9 & a,a9 // b,b9 by A2,Th36;
then
A5: b,b9 // c,c9 by A4,Def1;
b,c // b9,c9 by A2,A3,Th49;
hence thesis by A1,A5;
end;
theorem Th51:
a,b,c are_collinear & b<>c & parallelogram a,a9,b,b9 &
parallelogram a,a9,c,c9 implies parallelogram b,b9,c,c9
proof
assume that
A1: a,b,c are_collinear and
A2: b<>c and
A3: parallelogram a,a9,b,b9 and
A4: parallelogram a,a9,c,c9;
A5: b<>b9 by A3,Th36;
a,b // a,c by A1;
then
A6: a,b // b,c by Th7;
thus thesis by A2,A3,A4,A6,A5,Th23,Th50;
end;
theorem Th52:
parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 &
parallelogram b,b9,d,d9 implies c,d // c9,d9
proof
assume that
A1: parallelogram a,a9,b,b9 and
A2: parallelogram a,a9,c,c9 and
A3: parallelogram b,b9,d,d9;
A4: now
assume
A5: not a,a9,d are_collinear;
parallelogram b,b9,a,a9 by A1,Th43;
then parallelogram a,a9,d,d9 by A3,A5,Th50;
hence thesis by A2,Th49;
end;
A6: now
A7: ( not a,a9,b are_collinear)& a,a9 // a,a9 by A1,Th1;
A8: a<>a9 by A1,Th36;
assume that
A9: b,b9,c are_collinear and
A10: a,a9,d are_collinear;
a<>b by A1,Th36;
then consider x such that
A11: a,b,x are_collinear and
A12: x<>a and
A13: x<>b by Th48;
a,b // a,x by A11;
then consider y such that
A14: parallelogram a,a9,x,y by A12,A7,A8,Th23,Th44;
A15: not x,y,d are_collinear by A10,A14,Th39;
parallelogram b,b9,x,y by A1,A11,A13,A14,Th51;
then
A16: parallelogram x,y,d,d9 by A3,A15,Th50;
not x,y,c are_collinear by A1,A9,A11,A13,A14,Th39,Th51;
then parallelogram x,y,c,c9 by A2,A14,Th50;
hence thesis by A16,Th49;
end;
now
assume not b,b9,c are_collinear;
then parallelogram b,b9,c,c9 by A1,A2,Th50;
hence thesis by A3,Th49;
end;
hence thesis by A4,A6;
end;
Lm1: a<>b implies ex c,d st parallelogram a,b,c,d
proof
assume a<>b;
then consider c such that
A1: not a,b,c are_collinear by Th25;
ex d st parallelogram a,b,c,d by A1,Th44;
hence thesis;
end;
theorem
a<>d implies ex b,c st parallelogram a,b,c,d
proof
assume a<>d;
then consider b such that
A1: not a,d,b are_collinear by Th25;
not b,a,d are_collinear by A1,Th22;
then consider c such that
A2: parallelogram b,a,d,c by Th44;
parallelogram a,b,c,d by A2,Th43;
hence thesis;
end;
::
:: CONGRUENCE
::
definition
let SAS,a,b,r,s;
pred congr a,b,r,s means
a=b & r =s or ex p,q st parallelogram p,q,a, b & parallelogram p,q,r,s;
end;
theorem Th54:
congr a,a,b,c implies b=c
by Th36;
theorem Th55:
congr a,b,c,c implies a=b
by Th36;
theorem Th56:
congr a,b,b,a implies a=b
by Th47;
theorem Th57:
congr a,b,c,d implies a,b // c,d
proof
assume
A1: congr a,b,c,d;
now
assume a<>b;
then consider p,q such that
A2: parallelogram p,q,a,b and
A3: parallelogram p, q,c,d by A1;
A4: p,q // c,d by A3;
p<>q & p,q // a,b by A2,Th36;
hence thesis by A4,Def1;
end;
hence thesis by Th3;
end;
theorem Th58:
congr a,b,c,d implies a,c // b,d
proof
assume
A1: congr a,b,c,d;
then
A2: a<>b implies thesis by Th49;
now
assume
A3: a=b;
then c =d by A1,Th54;
hence thesis by A3,Th1;
end;
hence thesis by A2;
end;
theorem Th59:
congr a,b,c,d & not a,b,c are_collinear implies parallelogram a,b ,c,d
by Th57,Th58;
theorem Th60:
parallelogram a,b,c,d implies congr a,b,c,d
proof
A1: a,b // a,b by Th1;
assume
A2: parallelogram a,b,c,d;
then
A3: ( not a,c,b are_collinear)& a<>b by Th36,Th38;
a<>c by A2,Th36;
then consider p such that
A4: a,c,p are_collinear and
A5: a<>p and
A6: c <>p by Th48;
a,c // a,p by A4;
then consider q such that
A7: parallelogram a,p,b,q by A5,A1,A3,Th23,Th44;
parallelogram a,b,p,q by A7,Th43;
then parallelogram c,d,p,q by A2,A4,A6,Th51;
then
A8: parallelogram p,q,c,d by Th43;
parallelogram p,q,a,b by A7,Th43;
hence thesis by A8;
end;
theorem Th61:
congr a,b,c,d & a,b,c are_collinear & parallelogram r,s,a,b
implies parallelogram r,s,c,d
proof
assume that
A1: congr a,b,c,d and
A2: a,b,c are_collinear and
A3: parallelogram r,s,a,b;
now
A4: parallelogram a,b,r,s by A3,Th43;
assume
A5: a<>b;
then consider p,q such that
A6: parallelogram p,q,a,b and
A7: parallelogram p, q,c,d by A1;
parallelogram a,b,p,q by A6,Th43;
then
A8: r,c // s,d by A7,A4,Th52;
r,s // a,b & a,b // c,d by A1,A3,Th57;
then
A9: r,s // c,d by A5,Th8;
not r,s,c are_collinear by A2,A3,Th39;
hence thesis by A9,A8;
end;
hence thesis by A3,Th36;
end;
theorem Th62:
congr a,b,c,x & congr a,b,c,y implies x=y
proof
assume that
A1: congr a,b,c,x and
A2: congr a,b,c,y;
A3: now
assume that
a<>b and
A4: not a,b,c are_collinear;
parallelogram a,b,c,x & parallelogram a,b,c,y by A1,A2,A4,Th59;
hence thesis by Th45;
end;
A5: now
assume that
A6: a<>b and
A7: a,b,c are_collinear;
consider p,q such that
A8: parallelogram a,b,p,q by A6,Lm1;
parallelogram p,q,a,b by A8,Th43;
then parallelogram p,q,c,x & parallelogram p,q,c,y by A1,A2,A7,Th61;
hence thesis by Th45;
end;
now
assume
A9: a=b;
then c =x by A1,Th54;
hence thesis by A2,A9,Th54;
end;
hence thesis by A5,A3;
end;
theorem Th63:
ex d st congr a,b,c,d
proof
A1: now
assume a=b;
then congr a,b,c,c;
hence thesis;
end;
A2: now
assume that
A3: a<>b and
A4: a,b,c are_collinear;
consider p,q such that
A5: parallelogram a,b,p,q by A3,Lm1;
not p,q,c are_collinear by A4,A5,Th39;
then consider d such that
A6: parallelogram p,q,c,d by Th44;
parallelogram p,q,a,b by A5,Th43;
then congr a,b,c,d by A6;
hence thesis;
end;
now
assume that
a<>b and
A7: not a,b,c are_collinear;
ex d st parallelogram a,b,c,d by A7,Th44;
hence thesis by Th60;
end;
hence thesis by A1,A2;
end;
theorem Th64:
congr a,b,a,b
proof
now
assume a<>b;
then consider p,q such that
A1: parallelogram a,b,p,q by Lm1;
parallelogram p,q,a,b by A1,Th43;
hence thesis;
end;
hence thesis;
end;
theorem Th65:
congr r,s,a,b & congr r,s,c,d implies congr a,b,c,d
proof
assume that
A1: congr r,s,a,b and
A2: congr r,s,c,d;
A3: now
assume that
r<>s and
A4: ( not r,s,a are_collinear)& not r,s,c are_collinear;
parallelogram r,s,a,b & parallelogram r,s,c,d by A1,A2,A4,Th59;
hence thesis;
end;
A5: now
assume that
A6: r<>s and
A7: r,s,c are_collinear;
consider p,q such that
A8: parallelogram p,q,r,s and
A9: parallelogram p, q,a,b by A1,A6;
parallelogram p,q,c,d by A2,A7,A8,Th61;
hence thesis by A9;
end;
A10: now
assume that
A11: r<>s and
A12: r,s,a are_collinear;
consider p,q such that
A13: parallelogram p,q,r,s and
A14: parallelogram p,q,c,d by A2,A11;
parallelogram p,q,a,b by A1,A12,A13,Th61;
hence thesis by A14;
end;
r=s implies thesis by A1,A2,Th54;
hence thesis by A10,A5,A3;
end;
theorem
congr a,b,c,d implies congr c,d,a,b;
theorem Th67:
congr a,b,c,d implies congr b,a,d,c
proof
assume
A1: congr a,b,c,d;
A2: now
assume a<>b;
then consider p,q such that
A3: parallelogram p,q,a,b & parallelogram p, q,c,d by A1;
parallelogram q,p,b,a & parallelogram q,p,d,c by A3,Th43;
hence thesis;
end;
a=b implies thesis by A1,Th54;
hence thesis by A2;
end;
theorem Th68:
congr a,b,c,d implies congr a,c,b,d
proof
assume
A1: congr a,b,c,d;
A2: now
assume
A3: a=c;
congr a,b,a,b by Th64;
then b=d by A1,A3,Th62;
hence thesis by A3;
end;
A4: now
assume that
A5: a<>b and
A6: a<>c and
A7: a,b,c are_collinear;
A8: a,b // a,c by A7;
consider p,q such that
A9: parallelogram p,q,a,b and
A10: parallelogram p, q,c,d by A1,A5;
A11: a,p // a,p by Th1;
( not a,b,p are_collinear)& a<>p by A9,Th36,Th38;
then consider r such that
A12: parallelogram a,c,p,r by A6,A8,A11,Th23,Th44;
A13: a,c // p,r by A12;
A14: p,q // c,d by A10;
p<>q & p,q // a,b by A9,Th36;
then
A15: a,b // c,d by A14,Def1;
then a,c // b,d by A5,A7,Th32;
then
A16: p,r // b,d by A6,A13,Def1;
parallelogram p,r,a,c by A12,Th43;
then
A17: p,a // r,c;
p,a // q,b & p<>a by A9,Th36;
then
A18: r,c // q,b by A17,Def1;
p,c // q,d by A10;
then
A19: q,d // p,c by Th6;
p,q // a,b by A9;
then
A20: a,b // p,q by Th6;
A21: a,c // p,r by A12;
a,b // a,c by A7;
then a,c // p,q by A5,A20,Def1;
then p,q // p,r by A6,A21,Def1;
then
A22: r,q // r,p by Th7;
a,c,b are_collinear by A7,Th22;
then
A23: not p,r,b are_collinear by A12,Th39;
A24: parallelogram p,r,a,c by A12,Th43;
c,b // c,d by A5,A7,A15,Th33;
then b,c // b,d by Th7;
then p,b // r,d by A22,A18,A19,Def1;
then parallelogram p,r,b,d by A23,A16;
hence thesis by A24;
end;
A25: now
assume that
a<>b and
a<>c and
A26: not a,b,c are_collinear;
parallelogram a,b,c,d by A1,A26,Th59;
then parallelogram a,c,b,d by Th43;
hence thesis by Th60;
end;
now
assume
A27: a=b;
then c =d by A1,Th54;
hence thesis by A27,Th64;
end;
hence thesis by A2,A4,A25;
end;
theorem Th69:
congr a,b,c,d implies congr c,d,a,b & congr b,a,d,c & congr a,c,
b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a
proof
assume
A1: congr a,b,c,d;
then congr c,d,a,b;
then
A2: congr d,c,b,a by Th67;
congr b,a,d,c & congr a,c,b,d by A1,Th67,Th68;
hence thesis by A2,Th67,Th68;
end;
theorem Th70:
congr a,b,p,q & congr b,c,q,s implies congr a,c,p,s
proof
assume congr a,b,p,q & congr b,c,q,s;
then congr b,q,a,p & congr b,q,c,s by Th69;
then congr a,p,c,s by Th65;
hence thesis by Th68;
end;
theorem Th71:
congr b,a,p,q & congr c,a,p,r implies congr b,c,r,q
proof
assume that
A1: congr b,a,p,q and
A2: congr c,a,p,r;
A3: congr r,p,a,c by A2,Th69;
consider s such that
A4: congr p,q,r,s by Th63;
congr r,p,s,q by A4,Th69;
then
A5: congr a,c,s,q by A3,Th65;
congr p,q,b,a by A1;
then congr b,a,r,s by A4,Th65;
hence thesis by A5,Th70;
end;
theorem
congr a,o,o,p & congr b,o,o,q implies congr a,b,q,p by Th71;
theorem Th73:
congr b,a,p,q & congr c,a,p,r implies b,c // q,r
proof
assume congr b,a,p,q & congr c,a,p,r;
then congr b,c,r,q by Th71;
then b,c // r,q by Th57;
hence thesis by Th6;
end;
theorem
congr a,o,o,p & congr b,o,o,q implies a,b // p,q by Th73;
::
:: A VECTOR' GROUP
::
definition
let SAS,a,b,o;
func sum(a,b,o) -> Element of SAS means
:Def5:
congr o,a,b,it;
correctness by Th62,Th63;
end;
definition
let SAS,a,o;
func opposite(a,o) -> Element of SAS means
:Def6:
sum(a,it,o) = o;
existence
proof
consider b being Element of SAS such that
A1: congr a,o,o,b by Th63;
take b;
congr o,a,b,o by A1,Th67;
hence thesis by Def5;
end;
uniqueness
proof
let b1,b2 be Element of SAS such that
A2: sum(a,b1,o) = o and
A3: sum(a,b2,o) = o;
congr o,a,b2,o by A3,Def5;
then
A4: congr a,o,o,b2 by Th67;
congr o,a,b1,o by A2,Def5;
then congr a,o,o,b1 by Th67;
hence thesis by A4,Th62;
end;
end;
definition
let SAS,a,b,o;
func diff(a,b,o) -> Element of SAS equals
sum(a,opposite(b,o),o);
correctness;
end;
theorem Th75:
sum(a,o,o)=a
by Th64,Def5;
theorem
ex x st sum(a,x,o)=o
proof
consider x such that
A1: congr a,o,o,x by Th63;
A2: congr o,a,x,sum(a,x,o) by Def5;
congr o,a,x,o by A1,Th69;
hence thesis by A2,Th62;
end;
theorem
sum(sum(a,b,o),c,o)=sum(a,sum(b,c,o),o)
proof
congr o,a,b,sum(a,b,o) & congr o,a,sum(b,c,o),sum(a,sum(b,c,o),o) by Def5;
then
A1: congr b,sum(a,b,o),sum(b,c,o),sum(a,sum(b,c,o),o) by Th65;
congr o,b,c,sum(b,c,o) by Def5;
then
A2: congr b,o,sum(b,c,o) ,c by Th69;
congr o,sum(a,b,o),c,sum(sum(a,b,o),c,o) by Def5;
then congr b,sum(a,b,o),sum(b,c,o),sum(sum(a,b,o),c,o) by A2,Th70;
hence thesis by A1,Th62;
end;
theorem Th78:
sum(a,b,o)=sum(b,a,o)
proof
congr o,b,a,sum(b,a,o) by Def5;
then congr o,a,b,sum(b,a,o) by Th69;
hence thesis by Def5;
end;
theorem
sum(a,a,o)=o implies a=o
proof
assume sum(a,a,o)=o;
then congr o,a,a,o by Def5;
hence thesis by Th56;
end;
theorem
sum(a,x,o)=sum(a,y,o) implies x=y
proof
assume
A1: sum(a,x,o)=sum(a,y,o);
congr o,a,x,sum(a,x,o) by Def5;
then
A2: congr a,o,sum(a,x,o),x by Th69;
congr o,a,y,sum(a,y,o) by Def5;
then congr a,o,sum(a,x,o),y by A1,Th69;
hence thesis by A2,Th62;
end;
theorem Th81:
congr a,o,o,opposite(a,o)
proof
sum(a,opposite(a,o),o)=o & congr o,a,opposite(a,o),sum(a,opposite(a,o),o
) by Def5,Def6;
hence thesis by Th69;
end;
theorem Th82:
opposite(a,o)=opposite(b,o) implies a=b
proof
assume
A1: opposite(a,o)=opposite(b,o);
congr a,o,o,opposite(a,o) by Th81;
then
A2: congr opposite(a,o),o,o,a by Th69;
congr b,o,o,opposite(b,o) by Th81;
then congr opposite(a,o),o,o,b by A1,Th69;
hence thesis by A2,Th62;
end;
theorem
a,b // opposite(a,o),opposite(b,o)
proof
sum(b,opposite(b,o),o)=o by Def6;
then congr o,b,opposite(b,o),o by Def5;
then
A1: congr b,o,o,opposite(b,o) by Th69;
sum(a,opposite(a,o),o)=o by Def6;
then congr o,a,opposite(a,o),o by Def5;
then congr a,o,o,opposite(a,o) by Th69;
hence thesis by A1,Th73;
end;
theorem
opposite(o,o)=o
proof
sum(o,opposite(o,o),o)=o by Def6;
then sum(opposite(o,o),o,o)=o by Th78;
hence thesis by Th75;
end;
theorem Th85:
p,q // sum(p,r,o),sum(q,r,o)
proof
congr o,p,r,sum(p,r,o) by Def5;
then
A1: congr p,o,sum(p,r,o),r by Th69;
congr o,q,r,sum(q,r,o) by Def5;
then congr p,q,sum(p,r,o),sum(q,r,o) by A1,Th70;
hence thesis by Th57;
end;
theorem
p,q // r,s implies p,q // sum(p,r,o),sum(q,s,o)
proof
assume
A1: p,q // r,s;
now
consider t such that
A2: congr o,q,r,t by Th63;
assume that
A3: p<>q and
A4: r<>s;
congr o,q,s,sum(q,s,o) by Def5;
then congr r,t,s,sum(q,s,o) by A2,Th65;
then
A5: congr r,s,t,sum(q,s,o) by Th69;
then
A6: t<>sum(q,s,o) by A4,Th55;
r,s // t,sum(q,s,o) by A5,Th57;
then
A7: p,q // t,sum(q,s,o) by A1,A4,Th8;
congr o,p,r,sum(p,r,o) by Def5;
then congr p,o,sum(p,r,o),r by Th69;
then congr p,q,sum(p,r,o),t by A2,Th70;
then p,q // sum(p,r,o),t by Th57;
then p,q // t,sum(p,r,o) by Th6;
then t,sum(q,s,o) // t,sum(p,r,o) by A3,A7,Def1;
then t,sum(q,s,o) // sum(p,r,o),sum(q,s,o) by Th7;
hence thesis by A6,A7,Th8;
end;
hence thesis by Th3,Th85;
end;
theorem Th87:
diff(a,b,o)=o iff a=b
proof
diff(a,b,o)=o implies a=b
proof
assume diff(a,b,o)=o;
then opposite(a,o)= opposite(b,o) by Def6;
hence thesis by Th82;
end;
hence thesis by Def6;
end;
theorem Th88:
o,diff(b,a,o) // a,b
proof
congr a,o,o,opposite(a,o) by Th81;
then
A1: congr o,opposite(a,o),a,o;
congr o,b,opposite(a,o),sum(b,opposite(a,o),o) by Def5;
then congr o,opposite(a,o),b,diff(b,a,o) by Th69;
then congr a,o,b,diff(b,a,o) by A1,Th65;
then congr o,diff(b,a,o),a,b by Th69;
hence thesis by Th57;
end;
theorem
o,diff(b,a,o),diff(d,c,o) are_collinear iff a,b // c,d
proof
A1: a,b // c,d implies o,diff(b,a,o),diff(d,c,o) are_collinear
proof
assume
A2: a,b // c,d;
A3: now
o,diff(d,c,o) // c,d by Th88;
then
A4: c,d // o,diff(d,c,o) by Th6;
assume that
A5: a<>b and
A6: c <>d;
o,diff(b,a,o) // a,b by Th88;
then a,b // o,diff(b,a,o) by Th6;
then o,diff(b,a,o) // c,d by A2,A5,Def1;
then o,diff(b,a,o) // o,diff(d,c,o) by A6,A4,Th8;
hence thesis;
end;
now
assume a=b or c =d;
then o=diff(b,a,o) or o=diff(d,c,o) by Th87;
then o,diff(b,a,o) // o,diff(d,c,o) by Def1,Th3;
hence thesis;
end;
hence thesis by A3;
end;
o,diff(b,a,o),diff(d,c,o) are_collinear implies a,b // c,d
proof
assume
A7: o,diff(b,a,o),diff(d,c,o) are_collinear;
A8: now
A9: o,diff(d,c,o) // c,d by Th88;
assume that
A10: o<>diff(b,a,o) and
A11: o<>diff(d,c,o);
o,diff(b,a,o) // o,diff(d,c,o) & o,diff(b,a,o) // a,b by A7,Th88;
then o,diff(d,c,o) // a,b by A10,Def1;
hence thesis by A11,A9,Def1;
end;
now
assume o=diff(b,a,o) or o=diff(d,c,o);
then a=b or c =d by Th87;
hence thesis by Def1,Th3;
end;
hence thesis by A8;
end;
hence thesis by A1;
end;
::
:: A TRAPEZIUM RELATION
::
definition
let SAS,a,b,c,d,o;
pred trap a,b,c,d,o means
not o,a,c are_collinear & o,a,b are_collinear
& o,c,d are_collinear & a,c // b,d;
end;
definition
let SAS,o,p;
pred qtrap o,p means
for b,c holds ex d st ( o,p,b are_collinear
implies o,c,d are_collinear & p,c // b,d);
end;
theorem Th90:
trap a,b,c,d,o implies o<>a & a<>c & c <>o
by Th24;
theorem
trap a,b,c,x,o & trap a,b,c,y,o implies x=y
by Th34;
theorem
not o,a,b are_collinear implies trap a,o,b,o,o
by Def1,Th24;
theorem Th93:
trap a,b,c,d,o implies trap c,d,a,b,o
by Th22,Th6;
theorem Th94:
trap a,b,c,d,d implies d=b
proof
assume
A1: trap a,b,c,d,d;
then a,c // b,d;
then
A2: d,b // a,c by Th6;
d,a,b are_collinear by A1;
then d,a // d,b;
then
A3: d,b // a,d by Th6;
assume not thesis;
then a,d // a,c by A3,A2,Def1;
then
A4: d,a // d,c by Th7;
not d,a,c are_collinear by A1;
hence contradiction by A4;
end;
theorem Th95:
o<>b & trap a,b,c,d,o implies not o,b,d are_collinear
proof
assume that
A1: o<>b and
A2: trap a,b,c,d,o;
o,a,b are_collinear by A2;
then
A3: o,a // o,b;
o,c,d are_collinear by A2;
then
A4: o,c // o,d;
o<>d & not o,a,c are_collinear by A1,A2,Th94;
hence thesis by A1,A3,A4,Th23;
end;
theorem
o<>b & trap a,b,c,d,o implies trap b,a,d,c,o
by Th22,Th6,Th95;
theorem
trap a,b,c,d,b implies b=d by Th93,Th94;
theorem Th98:
trap a,p,b,q,o & trap a,p,c,r,o implies b,c // q,r
proof
assume that
A1: trap a,p,b,q,o and
A2: trap a,p,c,r,o;
not o,a,b are_collinear by A1;
then
A3: not o,a // o,b;
o,c,r are_collinear by A2;
then
A4: o,c //o,r;
not o,a,c are_collinear by A2;
then
A5: not o,a //o,c;
o,b,q are_collinear by A1;
then
A6: o,b //o,q;
o,a,p are_collinear by A1;
then
A7: o,a //o,p;
a,b // p,q & a,c // p,r by A1,A2;
hence thesis by A3,A7,A6,A5,A4,Def1;
end;
theorem Th99:
trap a,p,b,q,o & trap a,p,c,r,o & not o,b,c are_collinear
implies trap b,q,c,r,o
by Th98;
theorem
trap a,p,b,q,o & trap a,p,c,r,o & trap b,q,d,s,o implies c,d // r,s
proof
assume that
A1: trap a,p,b,q,o and
A2: trap a,p,c,r,o and
A3: trap b,q,d,s,o;
A4: now
assume
A5: not o,a,d are_collinear;
trap b,q,a,p,o by A1,Th93;
then trap a,p,d,s,o by A3,A5,Th99;
hence thesis by A2,Th98;
end;
A6: now
not o,a,b are_collinear by A1;
then not b,a,o are_collinear by Th22;
then consider x such that
A7: parallelogram b,a,o,x by Th44;
o,b,q are_collinear by A1;
then o,b // o,q;
then
A8: b,o // q,o by Th6;
A9: o,x // o,x by Th1;
b,o // a,x & b<>o by A7,Th36;
then
A10: q,o // a,x by A8,Def1;
A11: not o,x,b are_collinear by A7,Th38;
A12: o<>d by A3,Th90;
assume that
A13: o<>p and
A14: o,b,c are_collinear and
A15: o,a,d are_collinear;
not o,p,q are_collinear by A1,A13,Th95;
then not q,p,o are_collinear by Th22;
then consider y such that
A16: parallelogram q,p,o,y by Th44;
A17: not o,x,a are_collinear by A7,Th38;
A18: o<>c by A2,Th90;
a,b // p,q by A1;
then
A19: b,a // q,p by Th6;
A20: o,a,p are_collinear by A1;
b,a // o,x & b<>a by A7,Th36;
then
A21: q,p // o,x by A19,Def1;
A22: o<>x by A7,Th36;
q<>p & q,p // o,y by A16,Th36;
then o,x // o,y by A21,Def1;
then
A23: o,x,y are_collinear;
q,o // p,y & q<>o by A16,Th36;
then
A24: a,x // p,y by A10,Def1;
not o,a,x are_collinear by A7,Th38;
then
A25: trap a,p,x,y,o by A23,A24,A20;
not o,b,x are_collinear by A7,Th38;
then
A26: trap b,q,x,y,o by A1,A25,Th99;
o,a // o,d by A15;
then
A27: trap x,y,d,s,o by A3,A26,A22,A12,A17,A9,Th23,Th99;
o,b // o,c by A14;
then trap x,y,c,r,o by A2,A25,A11,A22,A18,A9,Th23,Th99;
hence thesis by A27,Th98;
end;
A28: now
assume
A29: o=p;
then o=q by A1,Th93,Th94;
then
A30: o=s by A3,Th93,Th94;
o=r by A2,A29,Th93,Th94;
hence thesis by A30,Def1;
end;
now
assume not o,b,c are_collinear;
then trap b,q,c,r,o by A1,A2,Th99;
hence thesis by A3,Th98;
end;
hence thesis by A4,A28,A6;
end;
theorem Th101:
for o,a holds ex p st o,a,p are_collinear & qtrap o,p
proof
let o,a;
consider p such that
A1: for b,c holds o,a // o,p & ex d st o,p // o,b implies o,c // o,d & p
,c // b,d by Def1;
take p;
now
thus o,a,p are_collinear by A1;
let b,c;
consider d such that
A2: o,p // o,b implies o,c // o,d & p,c // b,d by A1;
take d;
assume o,p,b are_collinear;
hence o,c,d are_collinear & p,c // b,d by A2;
end;
hence thesis;
end;
theorem Th102:
ex x,y,z st x<>y & y<>z & z<>x
proof
consider x,y,z such that
A1: not x,y // x,z by Def1;
take x,y,z;
thus thesis by A1,Def1,Th1,Th3;
end;
theorem Th103:
qtrap o,p implies o<>p
proof
ex b st o<>b
proof
consider x,y,z such that
A1: x<>y and
y<>z and
z<>x by Th102;
o<>x or o<>y or o<>z by A1;
hence thesis;
end;
then consider b such that
A2: o<>b;
consider c such that
A3: not o,b // o,c by A2,Th13;
assume qtrap o,p;
then consider d such that
A4: o,p,b are_collinear implies o,c,d are_collinear & p,c // b,d;
A5: now
assume that
A6: b<>d & not o,b // o,c and
A7: o,d // b,d and
A8: o,c // b,d;
d,o // d,b by A7,Th6;
hence b<>d & not o,b // o,c & b,d // o,b & b,d // o,c by A6,A8,Th6,Th7;
end;
assume not thesis;
then o,o // o,b implies o,c // o,d & o,c // b,d by A4;
then
b=d & not o,b // o,c & o,c // o,d or b<>d & o<>c & not o,b // o,c & o,c
// o,d & o,c // b,d by A3,Def1,Th3;
hence contradiction by A5,Def1,Th6;
end;
theorem
qtrap o,p implies ex q st not o,p,q are_collinear & qtrap o,q
proof
A1: o,p // o,p by Th1;
assume
A2: qtrap o,p;
then
A3: o<>p by Th103;
consider r such that
A4: not o,p,r are_collinear by A2,Th25,Th103;
consider q such that
A5: o,r,q are_collinear and
A6: qtrap o,q by Th101;
take q;
o<>q & o,r // o,q by A5,A6,Th103;
hence thesis by A3,A4,A6,A1,Th23;
end;
theorem
not o,p,c are_collinear & o,p,b are_collinear & qtrap o,p implies ex d
st trap p,b,c,d,o
proof
assume that
A1: ( not o,p,c are_collinear)& o,p,b are_collinear and
A2: qtrap o,p;
consider d such that
A3: o,p,b are_collinear implies o,c,d are_collinear & p,c // b,d by A2;
take d;
thus thesis by A1,A3;
end;