:: Semi-Affine Space :: by Eugeniusz Kusak and Krzysztof Radziszewski :: :: Received November 30, 1990 :: Copyright (c) 1990-2017 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;