:: DIRAF semantic presentation begin definition let X be non empty set ; let R be Relation of [:X,X:]; func lambda R -> Relation of [:X,X:] means :Def1: :: DIRAF:def 1 for a, b, c, d being Element of X holds ( [[a,b],[c,d]] in it iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ); existence ex b1 being Relation of [:X,X:] st for a, b, c, d being Element of X holds ( [[a,b],[c,d]] in b1 iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) proof defpred S1[ set , set ] means ex a, b, c, d being Element of X st ( \$1 = [a,b] & \$2 = [c,d] & ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ); set XX = [:X,X:]; consider P being Relation of [:X,X:],[:X,X:] such that A1: for x, y being set holds ( [x,y] in P iff ( x in [:X,X:] & y in [:X,X:] & S1[x,y] ) ) from RELSET_1:sch_1(); take P ; ::_thesis: for a, b, c, d being Element of X holds ( [[a,b],[c,d]] in P iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) let a, b, c, d be Element of X; ::_thesis: ( [[a,b],[c,d]] in P iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ( not [[a,b],[c,d]] in P or [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) proof assume [[a,b],[c,d]] in P ; ::_thesis: ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) then consider a9, b9, c9, d9 being Element of X such that A2: [a,b] = [a9,b9] and A3: [c,d] = [c9,d9] and A4: ( [[a9,b9],[c9,d9]] in R or [[a9,b9],[d9,c9]] in R ) by A1; c = c9 by A3, XTUPLE_0:1; hence ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) by A2, A3, A4, XTUPLE_0:1; ::_thesis: verum end; hence ( [[a,b],[c,d]] in P iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Relation of [:X,X:] st ( for a, b, c, d being Element of X holds ( [[a,b],[c,d]] in b1 iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ) & ( for a, b, c, d being Element of X holds ( [[a,b],[c,d]] in b2 iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ) holds b1 = b2 proof set XX = [:X,X:]; let P, Q be Relation of [:X,X:]; ::_thesis: ( ( for a, b, c, d being Element of X holds ( [[a,b],[c,d]] in P iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ) & ( for a, b, c, d being Element of X holds ( [[a,b],[c,d]] in Q iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ) implies P = Q ) assume that A5: for a, b, c, d being Element of X holds ( [[a,b],[c,d]] in P iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) and A6: for a, b, c, d being Element of X holds ( [[a,b],[c,d]] in Q iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ; ::_thesis: P = Q for x, y being set holds ( [x,y] in P iff [x,y] in Q ) proof let x, y be set ; ::_thesis: ( [x,y] in P iff [x,y] in Q ) A7: now__::_thesis:_(_[x,y]_in_Q_implies_[x,y]_in_P_) assume A8: [x,y] in Q ; ::_thesis: [x,y] in P then y in [:X,X:] by ZFMISC_1:87; then consider c, d being Element of X such that A9: y = [c,d] by DOMAIN_1:1; x in [:X,X:] by A8, ZFMISC_1:87; then A10: ex a, b being Element of X st x = [a,b] by DOMAIN_1:1; then ( [x,y] in Q iff ( [x,y] in R or [x,[d,c]] in R ) ) by A6, A9; hence [x,y] in P by A5, A8, A10, A9; ::_thesis: verum end; now__::_thesis:_(_[x,y]_in_P_implies_[x,y]_in_Q_) assume A11: [x,y] in P ; ::_thesis: [x,y] in Q then y in [:X,X:] by ZFMISC_1:87; then consider c, d being Element of X such that A12: y = [c,d] by DOMAIN_1:1; x in [:X,X:] by A11, ZFMISC_1:87; then A13: ex a, b being Element of X st x = [a,b] by DOMAIN_1:1; then ( [x,y] in P iff ( [x,y] in R or [x,[d,c]] in R ) ) by A5, A12; hence [x,y] in Q by A6, A11, A13, A12; ::_thesis: verum end; hence ( [x,y] in P iff [x,y] in Q ) by A7; ::_thesis: verum end; hence P = Q by RELAT_1:def_2; ::_thesis: verum end; end; :: deftheorem Def1 defines lambda DIRAF:def_1_:_ for X being non empty set for R, b3 being Relation of [:X,X:] holds ( b3 = lambda R iff for a, b, c, d being Element of X holds ( [[a,b],[c,d]] in b3 iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ); definition let S be non empty AffinStruct ; func Lambda S -> strict AffinStruct equals :: DIRAF:def 2 AffinStruct(# the carrier of S,(lambda the CONGR of S) #); correctness coherence AffinStruct(# the carrier of S,(lambda the CONGR of S) #) is strict AffinStruct ; ; end; :: deftheorem defines Lambda DIRAF:def_2_:_ for S being non empty AffinStruct holds Lambda S = AffinStruct(# the carrier of S,(lambda the CONGR of S) #); registration let S be non empty AffinStruct ; cluster Lambda S -> non empty strict ; coherence not Lambda S is empty ; end; theorem Th1: :: DIRAF:1 for S being OAffinSpace for x, y being Element of S holds x,y // x,y proof let S be OAffinSpace; ::_thesis: for x, y being Element of S holds x,y // x,y let x, y be Element of S; ::_thesis: x,y // x,y x,y // y,y by ANALOAF:def_5; hence x,y // x,y by ANALOAF:def_5; ::_thesis: verum end; Lm1: for S being OAffinSpace for x, y, z, t being Element of S st x,y // z,t holds z,t // x,y proof let S be OAffinSpace; ::_thesis: for x, y, z, t being Element of S st x,y // z,t holds z,t // x,y let x, y, z, t be Element of S; ::_thesis: ( x,y // z,t implies z,t // x,y ) assume A1: x,y // z,t ; ::_thesis: z,t // x,y now__::_thesis:_(_x_<>_y_implies_z,t_//_x,y_) assume A2: x <> y ; ::_thesis: z,t // x,y x,y // x,y by Th1; hence z,t // x,y by A1, A2, ANALOAF:def_5; ::_thesis: verum end; hence z,t // x,y by ANALOAF:def_5; ::_thesis: verum end; theorem Th2: :: DIRAF:2 for S being OAffinSpace for x, y, z, t being Element of S st x,y // z,t holds ( y,x // t,z & z,t // x,y & t,z // y,x ) proof let S be OAffinSpace; ::_thesis: for x, y, z, t being Element of S st x,y // z,t holds ( y,x // t,z & z,t // x,y & t,z // y,x ) let x, y, z, t be Element of S; ::_thesis: ( x,y // z,t implies ( y,x // t,z & z,t // x,y & t,z // y,x ) ) assume x,y // z,t ; ::_thesis: ( y,x // t,z & z,t // x,y & t,z // y,x ) hence ( y,x // t,z & z,t // x,y ) by Lm1, ANALOAF:def_5; ::_thesis: t,z // y,x hence t,z // y,x by ANALOAF:def_5; ::_thesis: verum end; theorem Th3: :: DIRAF:3 for S being OAffinSpace for z, t, x, y, u, w being Element of S st z <> t & x,y // z,t & z,t // u,w holds x,y // u,w proof let S be OAffinSpace; ::_thesis: for z, t, x, y, u, w being Element of S st z <> t & x,y // z,t & z,t // u,w holds x,y // u,w let z, t, x, y, u, w be Element of S; ::_thesis: ( z <> t & x,y // z,t & z,t // u,w implies x,y // u,w ) assume A1: z <> t ; ::_thesis: ( not x,y // z,t or not z,t // u,w or x,y // u,w ) assume that A2: x,y // z,t and A3: z,t // u,w ; ::_thesis: x,y // u,w z,t // x,y by A2, Th2; hence x,y // u,w by A1, A3, ANALOAF:def_5; ::_thesis: verum end; theorem Th4: :: DIRAF:4 for S being OAffinSpace for x, y, z being Element of S holds ( x,x // y,z & y,z // x,x ) proof let S be OAffinSpace; ::_thesis: for x, y, z being Element of S holds ( x,x // y,z & y,z // x,x ) let x, y, z be Element of S; ::_thesis: ( x,x // y,z & y,z // x,x ) y,z // x,x by ANALOAF:def_5; hence ( x,x // y,z & y,z // x,x ) by Th2; ::_thesis: verum end; theorem Th5: :: DIRAF:5 for S being OAffinSpace for x, y, z, t being Element of S st x,y // z,t & x,y // t,z & not x = y holds z = t proof let S be OAffinSpace; ::_thesis: for x, y, z, t being Element of S st x,y // z,t & x,y // t,z & not x = y holds z = t let x, y, z, t be Element of S; ::_thesis: ( x,y // z,t & x,y // t,z & not x = y implies z = t ) assume that A1: ( x,y // z,t & x,y // t,z & x <> y ) and A2: z <> t ; ::_thesis: contradiction z,t // t,z by A1, ANALOAF:def_5; hence contradiction by A2, ANALOAF:def_5; ::_thesis: verum end; theorem Th6: :: DIRAF:6 for S being OAffinSpace for x, y, z being Element of S holds ( x,y // x,z iff ( x,y // y,z or x,z // z,y ) ) proof let S be OAffinSpace; ::_thesis: for x, y, z being Element of S holds ( x,y // x,z iff ( x,y // y,z or x,z // z,y ) ) let x, y, z be Element of S; ::_thesis: ( x,y // x,z iff ( x,y // y,z or x,z // z,y ) ) now__::_thesis:_(_(_x,y_//_y,z_or_x,z_//_z,y_)_implies_x,y_//_x,z_) assume ( x,y // y,z or x,z // z,y ) ; ::_thesis: x,y // x,z then ( x,y // x,z or x,z // x,y ) by ANALOAF:def_5; hence x,y // x,z by Th2; ::_thesis: verum end; hence ( x,y // x,z iff ( x,y // y,z or x,z // z,y ) ) by ANALOAF:def_5; ::_thesis: verum end; definition let S be non empty AffinStruct ; let a, b, c be Element of S; pred Mid a,b,c means :Def3: :: DIRAF:def 3 a,b // b,c; end; :: deftheorem Def3 defines Mid DIRAF:def_3_:_ for S being non empty AffinStruct for a, b, c being Element of S holds ( Mid a,b,c iff a,b // b,c ); theorem Th7: :: DIRAF:7 for S being OAffinSpace for x, y, z being Element of S holds ( x,y // x,z iff ( Mid x,y,z or Mid x,z,y ) ) proof let S be OAffinSpace; ::_thesis: for x, y, z being Element of S holds ( x,y // x,z iff ( Mid x,y,z or Mid x,z,y ) ) let x, y, z be Element of S; ::_thesis: ( x,y // x,z iff ( Mid x,y,z or Mid x,z,y ) ) ( x,y // x,z iff ( x,y // y,z or x,z // z,y ) ) by Th6; hence ( x,y // x,z iff ( Mid x,y,z or Mid x,z,y ) ) by Def3; ::_thesis: verum end; theorem Th8: :: DIRAF:8 for S being OAffinSpace for a, b being Element of S st Mid a,b,a holds a = b proof let S be OAffinSpace; ::_thesis: for a, b being Element of S st Mid a,b,a holds a = b let a, b be Element of S; ::_thesis: ( Mid a,b,a implies a = b ) assume Mid a,b,a ; ::_thesis: a = b then a,b // b,a by Def3; hence a = b by ANALOAF:def_5; ::_thesis: verum end; theorem :: DIRAF:9 for S being OAffinSpace for a, b, c being Element of S st Mid a,b,c holds Mid c,b,a proof let S be OAffinSpace; ::_thesis: for a, b, c being Element of S st Mid a,b,c holds Mid c,b,a let a, b, c be Element of S; ::_thesis: ( Mid a,b,c implies Mid c,b,a ) assume Mid a,b,c ; ::_thesis: Mid c,b,a then a,b // b,c by Def3; then c,b // b,a by Th2; hence Mid c,b,a by Def3; ::_thesis: verum end; theorem :: DIRAF:10 for S being OAffinSpace for x, y being Element of S holds ( Mid x,x,y & Mid x,y,y ) proof let S be OAffinSpace; ::_thesis: for x, y being Element of S holds ( Mid x,x,y & Mid x,y,y ) let x, y be Element of S; ::_thesis: ( Mid x,x,y & Mid x,y,y ) ( x,x // x,y & x,y // y,y ) by Th4; hence ( Mid x,x,y & Mid x,y,y ) by Def3; ::_thesis: verum end; theorem :: DIRAF:11 for S being OAffinSpace for a, b, c, d being Element of S st Mid a,b,c & Mid a,c,d holds Mid b,c,d proof let S be OAffinSpace; ::_thesis: for a, b, c, d being Element of S st Mid a,b,c & Mid a,c,d holds Mid b,c,d let a, b, c, d be Element of S; ::_thesis: ( Mid a,b,c & Mid a,c,d implies Mid b,c,d ) assume that A1: Mid a,b,c and A2: Mid a,c,d ; ::_thesis: Mid b,c,d now__::_thesis:_(_a_<>_c_implies_Mid_b,c,d_) A3: a,b // b,c by A1, Def3; then a,b // a,c by ANALOAF:def_5; then A4: ( b,c // a,c or a = b ) by A3, ANALOAF:def_5; assume A5: a <> c ; ::_thesis: Mid b,c,d a,c // c,d by A2, Def3; then b,c // c,d by A5, A4, Th3; hence Mid b,c,d by Def3; ::_thesis: verum end; hence Mid b,c,d by A1, A2, Th8; ::_thesis: verum end; theorem :: DIRAF:12 for S being OAffinSpace for b, c, a, d being Element of S st b <> c & Mid a,b,c & Mid b,c,d holds Mid a,c,d proof let S be OAffinSpace; ::_thesis: for b, c, a, d being Element of S st b <> c & Mid a,b,c & Mid b,c,d holds Mid a,c,d let b, c, a, d be Element of S; ::_thesis: ( b <> c & Mid a,b,c & Mid b,c,d implies Mid a,c,d ) assume that A1: b <> c and A2: Mid a,b,c and A3: Mid b,c,d ; ::_thesis: Mid a,c,d now__::_thesis:_(_a_<>_b_implies_Mid_a,c,d_) assume A4: a <> b ; ::_thesis: Mid a,c,d A5: a,b // b,c by A2, Def3; b,c // c,d by A3, Def3; then A6: a,b // c,d by A1, A5, Th3; a,b // a,c by A5, ANALOAF:def_5; then a,c // c,d by A4, A6, ANALOAF:def_5; hence Mid a,c,d by Def3; ::_thesis: verum end; hence Mid a,c,d by A3; ::_thesis: verum end; theorem Th13: :: DIRAF:13 for S being OAffinSpace for x, y being Element of S ex z being Element of S st ( Mid x,y,z & y <> z ) proof let S be OAffinSpace; ::_thesis: for x, y being Element of S ex z being Element of S st ( Mid x,y,z & y <> z ) let x, y be Element of S; ::_thesis: ex z being Element of S st ( Mid x,y,z & y <> z ) consider z being Element of S such that A1: x,y // y,z and x,y // y,z and A2: y <> z by ANALOAF:def_5; Mid x,y,z by A1, Def3; hence ex z being Element of S st ( Mid x,y,z & y <> z ) by A2; ::_thesis: verum end; theorem :: DIRAF:14 for S being OAffinSpace for x, y, z being Element of S st Mid x,y,z & Mid y,x,z holds x = y proof let S be OAffinSpace; ::_thesis: for x, y, z being Element of S st Mid x,y,z & Mid y,x,z holds x = y let x, y, z be Element of S; ::_thesis: ( Mid x,y,z & Mid y,x,z implies x = y ) assume that A1: Mid x,y,z and A2: Mid y,x,z ; ::_thesis: x = y x,y // y,z by A1, Def3; then A3: x,y // x,z by ANALOAF:def_5; y,x // x,z by A2, Def3; then A4: x,y // z,x by ANALOAF:def_5; ( x = z implies x = y ) by A1, Th8; hence x = y by A3, A4, Th5; ::_thesis: verum end; theorem :: DIRAF:15 for S being OAffinSpace for x, y, z, t being Element of S st x <> y & Mid x,y,z & Mid x,y,t & not Mid y,z,t holds Mid y,t,z proof let S be OAffinSpace; ::_thesis: for x, y, z, t being Element of S st x <> y & Mid x,y,z & Mid x,y,t & not Mid y,z,t holds Mid y,t,z let x, y, z, t be Element of S; ::_thesis: ( x <> y & Mid x,y,z & Mid x,y,t & not Mid y,z,t implies Mid y,t,z ) assume A1: x <> y ; ::_thesis: ( not Mid x,y,z or not Mid x,y,t or Mid y,z,t or Mid y,t,z ) assume ( Mid x,y,z & Mid x,y,t ) ; ::_thesis: ( Mid y,z,t or Mid y,t,z ) then ( x,y // y,z & x,y // y,t ) by Def3; then y,z // y,t by A1, ANALOAF:def_5; hence ( Mid y,z,t or Mid y,t,z ) by Th7; ::_thesis: verum end; theorem :: DIRAF:16 for S being OAffinSpace for x, y, z, t being Element of S st x <> y & Mid x,y,z & Mid x,y,t & not Mid x,z,t holds Mid x,t,z proof let S be OAffinSpace; ::_thesis: for x, y, z, t being Element of S st x <> y & Mid x,y,z & Mid x,y,t & not Mid x,z,t holds Mid x,t,z let x, y, z, t be Element of S; ::_thesis: ( x <> y & Mid x,y,z & Mid x,y,t & not Mid x,z,t implies Mid x,t,z ) assume A1: x <> y ; ::_thesis: ( not Mid x,y,z or not Mid x,y,t or Mid x,z,t or Mid x,t,z ) assume that A2: Mid x,y,z and A3: Mid x,y,t ; ::_thesis: ( Mid x,z,t or Mid x,t,z ) x,y // y,t by A3, Def3; then A4: x,y // x,t by ANALOAF:def_5; x,y // y,z by A2, Def3; then x,y // x,z by ANALOAF:def_5; then x,z // x,t by A1, A4, ANALOAF:def_5; hence ( Mid x,z,t or Mid x,t,z ) by Th7; ::_thesis: verum end; theorem :: DIRAF:17 for S being OAffinSpace for x, y, t, z being Element of S st Mid x,y,t & Mid x,z,t & not Mid x,y,z holds Mid x,z,y proof let S be OAffinSpace; ::_thesis: for x, y, t, z being Element of S st Mid x,y,t & Mid x,z,t & not Mid x,y,z holds Mid x,z,y let x, y, t, z be Element of S; ::_thesis: ( Mid x,y,t & Mid x,z,t & not Mid x,y,z implies Mid x,z,y ) assume that A1: Mid x,y,t and A2: Mid x,z,t ; ::_thesis: ( Mid x,y,z or Mid x,z,y ) A3: x,z // z,t by A2, Def3; A4: x,y // y,t by A1, Def3; now__::_thesis:_(_x_<>_t_&_not_Mid_x,y,z_implies_Mid_x,z,y_) x,z // x,t by A3, ANALOAF:def_5; then A5: x,t // x,z by Th2; assume A6: x <> t ; ::_thesis: ( Mid x,y,z or Mid x,z,y ) x,y // x,t by A4, ANALOAF:def_5; then x,y // x,z by A6, A5, Th3; hence ( Mid x,y,z or Mid x,z,y ) by Th7; ::_thesis: verum end; hence ( Mid x,y,z or Mid x,z,y ) by A1, A2, Th8; ::_thesis: verum end; definition let S be non empty AffinStruct ; let a, b, c, d be Element of S; preda,b '||' c,d means :Def4: :: DIRAF:def 4 ( a,b // c,d or a,b // d,c ); end; :: deftheorem Def4 defines '||' DIRAF:def_4_:_ for S being non empty AffinStruct for a, b, c, d being Element of S holds ( a,b '||' c,d iff ( a,b // c,d or a,b // d,c ) ); theorem :: DIRAF:18 for S being OAffinSpace for a, b, c, d being Element of S holds ( a,b '||' c,d iff [[a,b],[c,d]] in lambda the CONGR of S ) proof let S be OAffinSpace; ::_thesis: for a, b, c, d being Element of S holds ( a,b '||' c,d iff [[a,b],[c,d]] in lambda the CONGR of S ) let a, b, c, d be Element of S; ::_thesis: ( a,b '||' c,d iff [[a,b],[c,d]] in lambda the CONGR of S ) thus ( a,b '||' c,d implies [[a,b],[c,d]] in lambda the CONGR of S ) ::_thesis: ( [[a,b],[c,d]] in lambda the CONGR of S implies a,b '||' c,d ) proof assume ( a,b // c,d or a,b // d,c ) ; :: according to DIRAF:def_4 ::_thesis: [[a,b],[c,d]] in lambda the CONGR of S then ( [[a,b],[c,d]] in the CONGR of S or [[a,b],[d,c]] in the CONGR of S ) by ANALOAF:def_2; hence [[a,b],[c,d]] in lambda the CONGR of S by Def1; ::_thesis: verum end; assume [[a,b],[c,d]] in lambda the CONGR of S ; ::_thesis: a,b '||' c,d then ( [[a,b],[c,d]] in the CONGR of S or [[a,b],[d,c]] in the CONGR of S ) by Def1; hence ( a,b // c,d or a,b // d,c ) by ANALOAF:def_2; :: according to DIRAF:def_4 ::_thesis: verum end; theorem Th19: :: DIRAF:19 for S being OAffinSpace for x, y being Element of S holds ( x,y '||' y,x & x,y '||' x,y ) proof let S be OAffinSpace; ::_thesis: for x, y being Element of S holds ( x,y '||' y,x & x,y '||' x,y ) let x, y be Element of S; ::_thesis: ( x,y '||' y,x & x,y '||' x,y ) x,y // x,y by Th1; hence ( x,y '||' y,x & x,y '||' x,y ) by Def4; ::_thesis: verum end; theorem Th20: :: DIRAF:20 for S being OAffinSpace for x, y, z being Element of S holds ( x,y '||' z,z & z,z '||' x,y ) proof let S be OAffinSpace; ::_thesis: for x, y, z being Element of S holds ( x,y '||' z,z & z,z '||' x,y ) let x, y, z be Element of S; ::_thesis: ( x,y '||' z,z & z,z '||' x,y ) ( x,y // z,z & z,z // x,y ) by Th4; hence ( x,y '||' z,z & z,z '||' x,y ) by Def4; ::_thesis: verum end; Lm2: for S being OAffinSpace for x, y, z, t, u, w being Element of S st x <> y & x,y '||' z,t & x,y '||' u,w holds z,t '||' u,w proof let S be OAffinSpace; ::_thesis: for x, y, z, t, u, w being Element of S st x <> y & x,y '||' z,t & x,y '||' u,w holds z,t '||' u,w let x, y, z, t, u, w be Element of S; ::_thesis: ( x <> y & x,y '||' z,t & x,y '||' u,w implies z,t '||' u,w ) assume that A1: x <> y and A2: x,y '||' z,t and A3: x,y '||' u,w ; ::_thesis: z,t '||' u,w A4: ( x,y // u,w or x,y // w,u ) by A3, Def4; A5: now__::_thesis:_(_x,y_//_t,z_implies_z,t_'||'_u,w_) assume x,y // t,z ; ::_thesis: z,t '||' u,w then ( t,z // u,w or t,z // w,u ) by A1, A4, ANALOAF:def_5; then ( z,t // w,u or z,t // u,w ) by ANALOAF:def_5; hence z,t '||' u,w by Def4; ::_thesis: verum end; now__::_thesis:_(_x,y_//_z,t_implies_z,t_'||'_u,w_) assume x,y // z,t ; ::_thesis: z,t '||' u,w then ( z,t // u,w or z,t // w,u ) by A1, A4, ANALOAF:def_5; hence z,t '||' u,w by Def4; ::_thesis: verum end; hence z,t '||' u,w by A2, A5, Def4; ::_thesis: verum end; theorem Th21: :: DIRAF:21 for S being OAffinSpace for x, y, z being Element of S st x,y '||' x,z holds y,x '||' y,z proof let S be OAffinSpace; ::_thesis: for x, y, z being Element of S st x,y '||' x,z holds y,x '||' y,z let x, y, z be Element of S; ::_thesis: ( x,y '||' x,z implies y,x '||' y,z ) A1: now__::_thesis:_(_x,y_//_z,x_&_x,y_'||'_x,z_implies_y,x_'||'_y,z_) assume x,y // z,x ; ::_thesis: ( x,y '||' x,z implies y,x '||' y,z ) then y,x // x,z by ANALOAF:def_5; then y,x // y,z by ANALOAF:def_5; hence ( x,y '||' x,z implies y,x '||' y,z ) by Def4; ::_thesis: verum end; A2: now__::_thesis:_(_x,y_//_x,z_&_x,y_'||'_x,z_implies_y,x_'||'_y,z_) A3: now__::_thesis:_(_x,z_//_z,y_&_x,y_'||'_x,z_implies_y,x_'||'_y,z_) assume x,z // z,y ; ::_thesis: ( x,y '||' x,z implies y,x '||' y,z ) then y,z // z,x by Th2; then y,z // y,x by ANALOAF:def_5; then y,x // y,z by Th2; hence ( x,y '||' x,z implies y,x '||' y,z ) by Def4; ::_thesis: verum end; A4: now__::_thesis:_(_x,y_//_y,z_&_x,y_'||'_x,z_implies_y,x_'||'_y,z_) assume x,y // y,z ; ::_thesis: ( x,y '||' x,z implies y,x '||' y,z ) then y,x // z,y by ANALOAF:def_5; hence ( x,y '||' x,z implies y,x '||' y,z ) by Def4; ::_thesis: verum end; assume x,y // x,z ; ::_thesis: ( x,y '||' x,z implies y,x '||' y,z ) hence ( x,y '||' x,z implies y,x '||' y,z ) by A4, A3, ANALOAF:def_5; ::_thesis: verum end; assume x,y '||' x,z ; ::_thesis: y,x '||' y,z hence y,x '||' y,z by A2, A1, Def4; ::_thesis: verum end; theorem Th22: :: DIRAF:22 for S being OAffinSpace for x, y, z, t being Element of S st x,y '||' z,t holds ( x,y '||' t,z & y,x '||' z,t & y,x '||' t,z & z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x ) proof let S be OAffinSpace; ::_thesis: for x, y, z, t being Element of S st x,y '||' z,t holds ( x,y '||' t,z & y,x '||' z,t & y,x '||' t,z & z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x ) let x, y, z, t be Element of S; ::_thesis: ( x,y '||' z,t implies ( x,y '||' t,z & y,x '||' z,t & y,x '||' t,z & z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x ) ) assume x,y '||' z,t ; ::_thesis: ( x,y '||' t,z & y,x '||' z,t & y,x '||' t,z & z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x ) then A1: ( x,y // z,t or x,y // t,z ) by Def4; hence x,y '||' t,z by Def4; ::_thesis: ( y,x '||' z,t & y,x '||' t,z & z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x ) ( y,x // t,z or y,x // z,t ) by A1, ANALOAF:def_5; hence ( y,x '||' z,t & y,x '||' t,z ) by Def4; ::_thesis: ( z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x ) ( z,t // x,y or z,t // y,x ) by A1, Th2; hence ( z,t '||' x,y & z,t '||' y,x ) by Def4; ::_thesis: ( t,z '||' x,y & t,z '||' y,x ) ( t,z // y,x or t,z // x,y ) by A1, Th2; hence ( t,z '||' x,y & t,z '||' y,x ) by Def4; ::_thesis: verum end; theorem Th23: :: DIRAF:23 for S being OAffinSpace for a, b, x, y, z, t being Element of S st a <> b & ( ( a,b '||' x,y & a,b '||' z,t ) or ( a,b '||' x,y & z,t '||' a,b ) or ( x,y '||' a,b & z,t '||' a,b ) or ( x,y '||' a,b & a,b '||' z,t ) ) holds x,y '||' z,t proof let S be OAffinSpace; ::_thesis: for a, b, x, y, z, t being Element of S st a <> b & ( ( a,b '||' x,y & a,b '||' z,t ) or ( a,b '||' x,y & z,t '||' a,b ) or ( x,y '||' a,b & z,t '||' a,b ) or ( x,y '||' a,b & a,b '||' z,t ) ) holds x,y '||' z,t let a, b, x, y, z, t be Element of S; ::_thesis: ( a <> b & ( ( a,b '||' x,y & a,b '||' z,t ) or ( a,b '||' x,y & z,t '||' a,b ) or ( x,y '||' a,b & z,t '||' a,b ) or ( x,y '||' a,b & a,b '||' z,t ) ) implies x,y '||' z,t ) assume that A1: a <> b and A2: ( ( a,b '||' x,y & a,b '||' z,t ) or ( a,b '||' x,y & z,t '||' a,b ) or ( x,y '||' a,b & z,t '||' a,b ) or ( x,y '||' a,b & a,b '||' z,t ) ) ; ::_thesis: x,y '||' z,t ( a,b '||' x,y & a,b '||' z,t ) by A2, Th22; hence x,y '||' z,t by A1, Lm2; ::_thesis: verum end; theorem Th24: :: DIRAF:24 for S being OAffinSpace holds not for x, y, z being Element of S holds x,y '||' x,z proof let S be OAffinSpace; ::_thesis: not for x, y, z being Element of S holds x,y '||' x,z consider x, y, z, t being Element of S such that A1: not x,y // z,t and A2: not x,y // t,z by ANALOAF:def_5; A3: x <> y by A1, Th4; now__::_thesis:_(_x,y_'||'_x,z_implies_not_x,y_'||'_x,t_) assume A4: x,y '||' x,z ; ::_thesis: not x,y '||' x,t thus not x,y '||' x,t ::_thesis: verum proof assume A5: x,y '||' x,t ; ::_thesis: contradiction then x,z '||' x,t by A3, A4, Th23; then z,x '||' z,t by Th21; then x,z '||' z,t by Th22; then ( x,y '||' z,t or x = z ) by A4, Th23; hence contradiction by A1, A2, A5, Def4; ::_thesis: verum end; end; hence not for x, y, z being Element of S holds x,y '||' x,z ; ::_thesis: verum end; theorem Th25: :: DIRAF:25 for S being OAffinSpace for x, z, y being Element of S ex t being Element of S st ( x,z '||' y,t & y <> t ) proof let S be OAffinSpace; ::_thesis: for x, z, y being Element of S ex t being Element of S st ( x,z '||' y,t & y <> t ) let x, z, y be Element of S; ::_thesis: ex t being Element of S st ( x,z '||' y,t & y <> t ) consider t being Element of S such that x,y // z,t and A1: x,z // y,t and A2: y <> t by ANALOAF:def_5; x,z '||' y,t by A1, Def4; hence ex t being Element of S st ( x,z '||' y,t & y <> t ) by A2; ::_thesis: verum end; theorem Th26: :: DIRAF:26 for S being OAffinSpace for x, y, z being Element of S ex t being Element of S st ( x,y '||' z,t & x,z '||' y,t ) proof let S be OAffinSpace; ::_thesis: for x, y, z being Element of S ex t being Element of S st ( x,y '||' z,t & x,z '||' y,t ) let x, y, z be Element of S; ::_thesis: ex t being Element of S st ( x,y '||' z,t & x,z '||' y,t ) consider t being Element of S such that A1: ( x,y // z,t & x,z // y,t ) and y <> t by ANALOAF:def_5; ( x,y '||' z,t & x,z '||' y,t ) by A1, Def4; hence ex t being Element of S st ( x,y '||' z,t & x,z '||' y,t ) ; ::_thesis: verum end; theorem Th27: :: DIRAF:27 for S being OAffinSpace for z, x, t, y being Element of S st z,x '||' x,t & x <> z holds ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) proof let S be OAffinSpace; ::_thesis: for z, x, t, y being Element of S st z,x '||' x,t & x <> z holds ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) let z, x, t, y be Element of S; ::_thesis: ( z,x '||' x,t & x <> z implies ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) ) assume that A1: z,x '||' x,t and A2: x <> z ; ::_thesis: ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) A3: now__::_thesis:_(_z,x_//_t,x_implies_ex_u_being_Element_of_S_st_ (_y,x_'||'_x,u_&_y,z_'||'_t,u_)_) consider p being Element of S such that A4: Mid z,x,p and A5: x <> p by Th13; A6: z,x // x,p by A4, Def3; then consider q being Element of S such that A7: y,x // x,q and A8: y,z // p,q by A2, ANALOAF:def_5; assume A9: z,x // t,x ; ::_thesis: ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) then x,p // t,x by A2, A6, ANALOAF:def_5; then p,x // x,t by Th2; then consider r being Element of S such that A10: q,x // x,r and A11: q,p // t,r by A5, ANALOAF:def_5; A12: now__::_thesis:_(_q_=_p_implies_ex_u_being_Element_of_S_st_ (_y,x_'||'_x,u_&_y,z_'||'_t,u_)_) assume q = p ; ::_thesis: ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) then A13: x,p // y,x by A7, Th2; x,p // z,x by A6, Th2; then z,x // y,x by A5, A13, ANALOAF:def_5; then y,x // t,x by A2, A9, ANALOAF:def_5; then A14: y,x '||' x,t by Def4; y,z // t,t by ANALOAF:def_5; then y,z '||' t,t by Def4; hence ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) by A14; ::_thesis: verum end; A15: now__::_thesis:_(_q_=_x_implies_ex_u_being_Element_of_S_st_ (_y,x_'||'_x,u_&_y,z_'||'_t,u_)_) A16: x,z // x,t by A9, Th2; assume A17: q = x ; ::_thesis: ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) p,x // x,z by A6, Th2; then y,z // x,z by A5, A8, A17, Th3; then y,z // x,t by A2, A16, Th3; then A18: y,z '||' t,x by Def4; y,x // x,x by Th4; then y,x '||' x,x by Def4; hence ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) by A18; ::_thesis: verum end; now__::_thesis:_(_q_<>_p_&_q_<>_x_implies_ex_u_being_Element_of_S_st_ (_y,x_'||'_x,u_&_y,z_'||'_t,u_)_) assume that A19: q <> p and A20: q <> x ; ::_thesis: ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) x,q // r,x by A10, Th2; then y,x // r,x by A7, A20, Th3; then A21: y,x '||' x,r by Def4; p,q // r,t by A11, Th2; then y,z // r,t by A8, A19, Th3; then y,z '||' t,r by Def4; hence ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) by A21; ::_thesis: verum end; hence ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) by A12, A15; ::_thesis: verum end; now__::_thesis:_(_z,x_//_x,t_implies_ex_u_being_Element_of_S_st_ (_y,x_'||'_x,u_&_y,z_'||'_t,u_)_) assume z,x // x,t ; ::_thesis: ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) then consider u being Element of S such that A22: ( y,x // x,u & y,z // t,u ) by A2, ANALOAF:def_5; ( y,x '||' x,u & y,z '||' t,u ) by A22, Def4; hence ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) ; ::_thesis: verum end; hence ex u being Element of S st ( y,x '||' x,u & y,z '||' t,u ) by A1, A3, Def4; ::_thesis: verum end; definition let S be non empty AffinStruct ; let a, b, c be Element of S; pred LIN a,b,c means :Def5: :: DIRAF:def 5 a,b '||' a,c; end; :: deftheorem Def5 defines LIN DIRAF:def_5_:_ for S being non empty AffinStruct for a, b, c being Element of S holds ( LIN a,b,c iff a,b '||' a,c ); notation let S be non empty AffinStruct ; let a, b, c be Element of S; synonym a,b,c is_collinear for LIN a,b,c; end; theorem :: DIRAF:28 for S being OAffinSpace for a, b, c being Element of S st Mid a,b,c holds a,b,c is_collinear proof let S be OAffinSpace; ::_thesis: for a, b, c being Element of S st Mid a,b,c holds a,b,c is_collinear let a, b, c be Element of S; ::_thesis: ( Mid a,b,c implies a,b,c is_collinear ) assume Mid a,b,c ; ::_thesis: a,b,c is_collinear then a,b // b,c by Def3; then a,b // a,c by ANALOAF:def_5; then a,b '||' a,c by Def4; hence a,b,c is_collinear by Def5; ::_thesis: verum end; theorem :: DIRAF:29 for S being OAffinSpace for a, b, c being Element of S holds ( not a,b,c is_collinear or Mid a,b,c or Mid b,a,c or Mid a,c,b ) proof let S be OAffinSpace; ::_thesis: for a, b, c being Element of S holds ( not a,b,c is_collinear or Mid a,b,c or Mid b,a,c or Mid a,c,b ) let a, b, c be Element of S; ::_thesis: ( not a,b,c is_collinear or Mid a,b,c or Mid b,a,c or Mid a,c,b ) A1: now__::_thesis:_(_a,b_//_c,a_implies_Mid_b,a,c_) assume a,b // c,a ; ::_thesis: Mid b,a,c then b,a // a,c by ANALOAF:def_5; hence Mid b,a,c by Def3; ::_thesis: verum end; assume a,b,c is_collinear ; ::_thesis: ( Mid a,b,c or Mid b,a,c or Mid a,c,b ) then A2: a,b '||' a,c by Def5; ( not a,b // a,c or Mid a,b,c or Mid a,c,b ) by Th7; hence ( Mid a,b,c or Mid b,a,c or Mid a,c,b ) by A2, A1, Def4; ::_thesis: verum end; Lm3: for S being OAffinSpace for x, y, z being Element of S st x,y,z is_collinear holds ( x,z,y is_collinear & y,x,z is_collinear ) proof let S be OAffinSpace; ::_thesis: for x, y, z being Element of S st x,y,z is_collinear holds ( x,z,y is_collinear & y,x,z is_collinear ) let x, y, z be Element of S; ::_thesis: ( x,y,z is_collinear implies ( x,z,y is_collinear & y,x,z is_collinear ) ) assume x,y,z is_collinear ; ::_thesis: ( x,z,y is_collinear & y,x,z is_collinear ) then x,y '||' x,z by Def5; then ( x,z '||' x,y & y,x '||' y,z ) by Th21, Th22; hence ( x,z,y is_collinear & y,x,z is_collinear ) by Def5; ::_thesis: verum end; theorem Th30: :: DIRAF:30 for S being OAffinSpace for x, y, z being Element of S st x,y,z is_collinear holds ( x,z,y is_collinear & y,x,z is_collinear & y,z,x is_collinear & z,x,y is_collinear & z,y,x is_collinear ) proof let S be OAffinSpace; ::_thesis: for x, y, z being Element of S st x,y,z is_collinear holds ( x,z,y is_collinear & y,x,z is_collinear & y,z,x is_collinear & z,x,y is_collinear & z,y,x is_collinear ) let x, y, z be Element of S; ::_thesis: ( x,y,z is_collinear implies ( x,z,y is_collinear & y,x,z is_collinear & y,z,x is_collinear & z,x,y is_collinear & z,y,x is_collinear ) ) assume x,y,z is_collinear ; ::_thesis: ( x,z,y is_collinear & y,x,z is_collinear & y,z,x is_collinear & z,x,y is_collinear & z,y,x is_collinear ) hence ( x,z,y is_collinear & y,x,z is_collinear ) by Lm3; ::_thesis: ( y,z,x is_collinear & z,x,y is_collinear & z,y,x is_collinear ) hence ( y,z,x is_collinear & z,x,y is_collinear ) by Lm3; ::_thesis: z,y,x is_collinear hence z,y,x is_collinear by Lm3; ::_thesis: verum end; theorem Th31: :: DIRAF:31 for S being OAffinSpace for x, y being Element of S holds ( x,x,y is_collinear & x,y,y is_collinear & x,y,x is_collinear ) proof let S be OAffinSpace; ::_thesis: for x, y being Element of S holds ( x,x,y is_collinear & x,y,y is_collinear & x,y,x is_collinear ) let x, y be Element of S; ::_thesis: ( x,x,y is_collinear & x,y,y is_collinear & x,y,x is_collinear ) A1: x,y '||' x,x by Th20; ( x,x '||' x,y & x,y '||' x,y ) by Th19, Th20; hence ( x,x,y is_collinear & x,y,y is_collinear & x,y,x is_collinear ) by A1, Def5; ::_thesis: verum end; theorem Th32: :: DIRAF:32 for S being OAffinSpace for x, y, z, t, u being Element of S st x <> y & x,y,z is_collinear & x,y,t is_collinear & x,y,u is_collinear holds z,t,u is_collinear proof let S be OAffinSpace; ::_thesis: for x, y, z, t, u being Element of S st x <> y & x,y,z is_collinear & x,y,t is_collinear & x,y,u is_collinear holds z,t,u is_collinear let x, y, z, t, u be Element of S; ::_thesis: ( x <> y & x,y,z is_collinear & x,y,t is_collinear & x,y,u is_collinear implies z,t,u is_collinear ) assume that A1: x <> y and A2: x,y,z is_collinear and A3: x,y,t is_collinear and A4: x,y,u is_collinear ; ::_thesis: z,t,u is_collinear A5: now__::_thesis:_(_x_<>_z_implies_z,t,u_is_collinear_) A6: x,y '||' x,z by A2, Def5; x,y '||' x,u by A4, Def5; then x,z '||' x,u by A1, A6, Th23; then A7: z,x '||' z,u by Th21; x,y '||' x,t by A3, Def5; then x,z '||' x,t by A1, A6, Th23; then A8: z,x '||' z,t by Th21; assume x <> z ; ::_thesis: z,t,u is_collinear then z,t '||' z,u by A8, A7, Th23; hence z,t,u is_collinear by Def5; ::_thesis: verum end; now__::_thesis:_(_x_=_z_implies_z,t,u_is_collinear_) assume A9: x = z ; ::_thesis: z,t,u is_collinear then ( z,y '||' z,t & z,y '||' z,u ) by A3, A4, Def5; then z,t '||' z,u by A1, A9, Th23; hence z,t,u is_collinear by Def5; ::_thesis: verum end; hence z,t,u is_collinear by A5; ::_thesis: verum end; theorem :: DIRAF:33 for S being OAffinSpace for x, y, z, t being Element of S st x <> y & x,y,z is_collinear & x,y '||' z,t holds x,y,t is_collinear proof let S be OAffinSpace; ::_thesis: for x, y, z, t being Element of S st x <> y & x,y,z is_collinear & x,y '||' z,t holds x,y,t is_collinear let x, y, z, t be Element of S; ::_thesis: ( x <> y & x,y,z is_collinear & x,y '||' z,t implies x,y,t is_collinear ) assume that A1: x <> y and A2: x,y,z is_collinear and A3: x,y '||' z,t ; ::_thesis: x,y,t is_collinear now__::_thesis:_(_z_<>_x_implies_x,y,t_is_collinear_) x,y '||' x,z by A2, Def5; then x,z '||' z,t by A1, A3, Th23; then z,x '||' z,t by Th22; then z,x,t is_collinear by Def5; then A4: x,z,t is_collinear by Th30; assume A5: z <> x ; ::_thesis: x,y,t is_collinear ( x,z,y is_collinear & x,z,x is_collinear ) by A2, Th30, Th31; hence x,y,t is_collinear by A5, A4, Th32; ::_thesis: verum end; hence x,y,t is_collinear by A3, Def5; ::_thesis: verum end; theorem :: DIRAF:34 for S being OAffinSpace for x, y, z, t being Element of S st x,y,z is_collinear & x,y,t is_collinear holds x,y '||' z,t proof let S be OAffinSpace; ::_thesis: for x, y, z, t being Element of S st x,y,z is_collinear & x,y,t is_collinear holds x,y '||' z,t let x, y, z, t be Element of S; ::_thesis: ( x,y,z is_collinear & x,y,t is_collinear implies x,y '||' z,t ) assume A1: ( x,y,z is_collinear & x,y,t is_collinear ) ; ::_thesis: x,y '||' z,t now__::_thesis:_(_x_<>_y_implies_x,y_'||'_z,t_) A2: ( x,y '||' x,z & x,y '||' x,t ) by A1, Def5; assume x <> y ; ::_thesis: x,y '||' z,t then x,z '||' x,t by A2, Th23; then z,x '||' z,t by Th21; then x,z '||' z,t by Th22; hence x,y '||' z,t by A2, Th23; ::_thesis: verum end; hence x,y '||' z,t by Th20; ::_thesis: verum end; theorem :: DIRAF:35 for S being OAffinSpace for u, z, x, y, w being Element of S st u <> z & x,y,u is_collinear & x,y,z is_collinear & u,z,w is_collinear holds x,y,w is_collinear proof let S be OAffinSpace; ::_thesis: for u, z, x, y, w being Element of S st u <> z & x,y,u is_collinear & x,y,z is_collinear & u,z,w is_collinear holds x,y,w is_collinear let u, z, x, y, w be Element of S; ::_thesis: ( u <> z & x,y,u is_collinear & x,y,z is_collinear & u,z,w is_collinear implies x,y,w is_collinear ) assume that A1: u <> z and A2: ( x,y,u is_collinear & x,y,z is_collinear ) and A3: u,z,w is_collinear ; ::_thesis: x,y,w is_collinear now__::_thesis:_(_x_<>_y_implies_x,y,w_is_collinear_) assume A4: x <> y ; ::_thesis: x,y,w is_collinear x,y,x is_collinear by Th31; then A5: z,u,x is_collinear by A2, A4, Th32; x,y,y is_collinear by Th31; then A6: z,u,y is_collinear by A2, A4, Th32; z,u,w is_collinear by A3, Th30; hence x,y,w is_collinear by A1, A6, A5, Th32; ::_thesis: verum end; hence x,y,w is_collinear by Th31; ::_thesis: verum end; theorem Th36: :: DIRAF:36 for S being OAffinSpace holds not for x, y, z being Element of S holds x,y,z is_collinear proof let S be OAffinSpace; ::_thesis: not for x, y, z being Element of S holds x,y,z is_collinear consider x, y, z being Element of S such that A1: not x,y '||' x,z by Th24; not x,y,z is_collinear by A1, Def5; hence not for x, y, z being Element of S holds x,y,z is_collinear ; ::_thesis: verum end; theorem :: DIRAF:37 for S being OAffinSpace for x, y being Element of S st x <> y holds ex z being Element of S st not x,y,z is_collinear proof let S be OAffinSpace; ::_thesis: for x, y being Element of S st x <> y holds ex z being Element of S st not x,y,z is_collinear let x, y be Element of S; ::_thesis: ( x <> y implies ex z being Element of S st not x,y,z is_collinear ) assume A1: x <> y ; ::_thesis: not for z being Element of S holds x,y,z is_collinear consider a, b, c being Element of S such that A2: not a,b,c is_collinear by Th36; assume A3: for z being Element of S holds x,y,z is_collinear ; ::_thesis: contradiction then A4: x,y,c is_collinear ; ( x,y,a is_collinear & x,y,b is_collinear ) by A3; hence contradiction by A1, A2, A4, Th32; ::_thesis: verum end; theorem Th38: :: DIRAF:38 for S being OAffinSpace for AS being non empty AffinStruct st AS = Lambda S holds for a, b, c, d being Element of S for a9, b9, c9, d9 being Element of AS st a = a9 & b = b9 & c = c9 & d = d9 holds ( a9,b9 // c9,d9 iff a,b '||' c,d ) proof let S be OAffinSpace; ::_thesis: for AS being non empty AffinStruct st AS = Lambda S holds for a, b, c, d being Element of S for a9, b9, c9, d9 being Element of AS st a = a9 & b = b9 & c = c9 & d = d9 holds ( a9,b9 // c9,d9 iff a,b '||' c,d ) let AS be non empty AffinStruct ; ::_thesis: ( AS = Lambda S implies for a, b, c, d being Element of S for a9, b9, c9, d9 being Element of AS st a = a9 & b = b9 & c = c9 & d = d9 holds ( a9,b9 // c9,d9 iff a,b '||' c,d ) ) assume A1: AS = Lambda S ; ::_thesis: for a, b, c, d being Element of S for a9, b9, c9, d9 being Element of AS st a = a9 & b = b9 & c = c9 & d = d9 holds ( a9,b9 // c9,d9 iff a,b '||' c,d ) let a, b, c, d be Element of S; ::_thesis: for a9, b9, c9, d9 being Element of AS st a = a9 & b = b9 & c = c9 & d = d9 holds ( a9,b9 // c9,d9 iff a,b '||' c,d ) let a9, b9, c9, d9 be Element of AS; ::_thesis: ( a = a9 & b = b9 & c = c9 & d = d9 implies ( a9,b9 // c9,d9 iff a,b '||' c,d ) ) assume A2: ( a = a9 & b = b9 & c = c9 & d = d9 ) ; ::_thesis: ( a9,b9 // c9,d9 iff a,b '||' c,d ) thus ( a9,b9 // c9,d9 implies a,b '||' c,d ) ::_thesis: ( a,b '||' c,d implies a9,b9 // c9,d9 ) proof assume A3: [[a9,b9],[c9,d9]] in the CONGR of AS ; :: according to ANALOAF:def_2 ::_thesis: a,b '||' c,d assume not [[a,b],[c,d]] in the CONGR of S ; :: according to ANALOAF:def_2,DIRAF:def_4 ::_thesis: a,b // d,c hence [[a,b],[d,c]] in the CONGR of S by A1, A2, A3, Def1; :: according to ANALOAF:def_2 ::_thesis: verum end; assume a,b '||' c,d ; ::_thesis: a9,b9 // c9,d9 then ( a,b // c,d or a,b // d,c ) by Def4; then ( [[a,b],[c,d]] in the CONGR of S or [[a,b],[d,c]] in the CONGR of S ) by ANALOAF:def_2; hence [[a9,b9],[c9,d9]] in the CONGR of AS by A1, A2, Def1; :: according to ANALOAF:def_2 ::_thesis: verum end; theorem Th39: :: DIRAF:39 for S being OAffinSpace for AS being non empty AffinStruct st AS = Lambda S holds ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ) ) proof let S be OAffinSpace; ::_thesis: for AS being non empty AffinStruct st AS = Lambda S holds ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ) ) let AS be non empty AffinStruct ; ::_thesis: ( AS = Lambda S implies ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ) ) ) assume A1: AS = Lambda S ; ::_thesis: ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ) ) hence ex x, y being Element of AS st x <> y by STRUCT_0:def_10; ::_thesis: ( ( for x, y, z, t, u, w being Element of AS holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ) ) thus for x, y, z, t, u, w being Element of AS holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ::_thesis: ( not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ) ) proof let x, y, z, t, u, w be Element of AS; ::_thesis: ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) reconsider x9 = x, y9 = y, z9 = z, t9 = t, u9 = u, w9 = w as Element of S by A1; ( x9,y9 '||' y9,x9 & x9,y9 '||' z9,z9 ) by Th19, Th20; hence ( x,y // y,x & x,y // z,z ) by A1, Th38; ::_thesis: ( ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ( x9 <> y9 & x9,y9 '||' z9,t9 & x9,y9 '||' u9,w9 implies z9,t9 '||' u9,w9 ) by Lm2; hence ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) by A1, Th38; ::_thesis: ( x,y // x,z implies y,x // y,z ) ( x9,y9 '||' x9,z9 implies y9,x9 '||' y9,z9 ) by Th21; hence ( x,y // x,z implies y,x // y,z ) by A1, Th38; ::_thesis: verum end; thus not for x, y, z being Element of AS holds x,y // x,z ::_thesis: ( ( for x, y, z being Element of AS ex t being Element of AS st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ) ) proof consider x9, y9, z9 being Element of S such that A2: not x9,y9 '||' x9,z9 by Th24; reconsider x = x9, y = y9, z = z9 as Element of AS by A1; not x,y // x,z by A1, A2, Th38; hence not for x, y, z being Element of AS holds x,y // x,z ; ::_thesis: verum end; thus for x, y, z being Element of AS ex t being Element of AS st ( x,z // y,t & y <> t ) ::_thesis: ( ( for x, y, z being Element of AS ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ) ) proof let x, y, z be Element of AS; ::_thesis: ex t being Element of AS st ( x,z // y,t & y <> t ) reconsider x9 = x, y9 = y, z9 = z as Element of S by A1; consider t9 being Element of S such that A3: x9,z9 '||' y9,t9 and A4: y9 <> t9 by Th25; reconsider t = t9 as Element of AS by A1; x,z // y,t by A1, A3, Th38; hence ex t being Element of AS st ( x,z // y,t & y <> t ) by A4; ::_thesis: verum end; thus for x, y, z being Element of AS ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ::_thesis: for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) proof let x, y, z be Element of AS; ::_thesis: ex t being Element of AS st ( x,y // z,t & x,z // y,t ) reconsider x9 = x, y9 = y, z9 = z as Element of S by A1; consider t9 being Element of S such that A5: ( x9,y9 '||' z9,t9 & x9,z9 '||' y9,t9 ) by Th26; reconsider t = t9 as Element of AS by A1; ( x,y // z,t & x,z // y,t ) by A1, A5, Th38; hence ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ; ::_thesis: verum end; thus for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ::_thesis: verum proof let x, y, z, t be Element of AS; ::_thesis: ( z,x // x,t & x <> z implies ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ) assume that A6: z,x // x,t and A7: x <> z ; ::_thesis: ex u being Element of AS st ( y,x // x,u & y,z // t,u ) reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of S by A1; z9,x9 '||' x9,t9 by A1, A6, Th38; then consider u9 being Element of S such that A8: ( y9,x9 '||' x9,u9 & y9,z9 '||' t9,u9 ) by A7, Th27; reconsider u = u9 as Element of AS by A1; ( y,x // x,u & y,z // t,u ) by A1, A8, Th38; hence ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ; ::_thesis: verum end; end; definition let IT be non empty AffinStruct ; attrIT is AffinSpace-like means :Def6: :: DIRAF:def 6 ( ( for x, y, z, t, u, w being Element of IT holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of IT holds x,y // x,z & ( for x, y, z being Element of IT ex t being Element of IT st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of IT ex t being Element of IT st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of IT st z,x // x,t & x <> z holds ex u being Element of IT st ( y,x // x,u & y,z // t,u ) ) ); end; :: deftheorem Def6 defines AffinSpace-like DIRAF:def_6_:_ for IT being non empty AffinStruct holds ( IT is AffinSpace-like iff ( ( for x, y, z, t, u, w being Element of IT holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of IT holds x,y // x,z & ( for x, y, z being Element of IT ex t being Element of IT st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of IT ex t being Element of IT st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of IT st z,x // x,t & x <> z holds ex u being Element of IT st ( y,x // x,u & y,z // t,u ) ) ) ); registration cluster non empty non trivial strict AffinSpace-like for AffinStruct ; existence ex b1 being non trivial AffinStruct st ( b1 is strict & b1 is AffinSpace-like ) proof set S = the OAffinSpace; A1: ( ( for x, y, z being Element of (Lambda the OAffinSpace) ex t being Element of (Lambda the OAffinSpace) st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of (Lambda the OAffinSpace) ex t being Element of (Lambda the OAffinSpace) st ( x,y // z,t & x,z // y,t ) ) ) by Th39; A2: for x, y, z, t being Element of (Lambda the OAffinSpace) st z,x // x,t & x <> z holds ex u being Element of (Lambda the OAffinSpace) st ( y,x // x,u & y,z // t,u ) by Th39; ( ( for x, y, z, t, u, w being Element of (Lambda the OAffinSpace) holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of (Lambda the OAffinSpace) holds x,y // x,z ) by Th39; then ( not Lambda the OAffinSpace is trivial & Lambda the OAffinSpace is AffinSpace-like ) by A1, A2, Def6; hence ex b1 being non trivial AffinStruct st ( b1 is strict & b1 is AffinSpace-like ) ; ::_thesis: verum end; end; definition mode AffinSpace is non trivial AffinSpace-like AffinStruct ; end; theorem :: DIRAF:40 for AS being AffinSpace holds ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ) ) by Def6, STRUCT_0:def_10; theorem Th41: :: DIRAF:41 for S being OAffinSpace holds Lambda S is AffinSpace proof let S be OAffinSpace; ::_thesis: Lambda S is AffinSpace set AS = Lambda S; A1: ( ( for x, y, z being Element of (Lambda S) ex t being Element of (Lambda S) st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of (Lambda S) ex t being Element of (Lambda S) st ( x,y // z,t & x,z // y,t ) ) ) by Th39; A2: for x, y, z, t being Element of (Lambda S) st z,x // x,t & x <> z holds ex u being Element of (Lambda S) st ( y,x // x,u & y,z // t,u ) by Th39; ( ( for x, y, z, t, u, w being Element of (Lambda S) holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of (Lambda S) holds x,y // x,z ) by Th39; hence Lambda S is AffinSpace by A1, A2, Def6; ::_thesis: verum end; theorem :: DIRAF:42 for AS being non empty AffinStruct holds ( ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ) ) iff AS is AffinSpace ) by Def6, STRUCT_0:def_10; theorem Th43: :: DIRAF:43 for S being OAffinPlane for x, y, z, t being Element of S st not x,y '||' z,t holds ex u being Element of S st ( x,y '||' x,u & z,t '||' z,u ) proof let S be OAffinPlane; ::_thesis: for x, y, z, t being Element of S st not x,y '||' z,t holds ex u being Element of S st ( x,y '||' x,u & z,t '||' z,u ) let x, y, z, t be Element of S; ::_thesis: ( not x,y '||' z,t implies ex u being Element of S st ( x,y '||' x,u & z,t '||' z,u ) ) assume not x,y '||' z,t ; ::_thesis: ex u being Element of S st ( x,y '||' x,u & z,t '||' z,u ) then ( not x,y // z,t & not x,y // t,z ) by Def4; then consider u being Element of S such that A1: ( ( x,y // x,u or x,y // u,x ) & ( z,t // z,u or z,t // u,z ) ) by ANALOAF:def_6; ( x,y '||' x,u & z,t '||' z,u ) by A1, Def4; hence ex u being Element of S st ( x,y '||' x,u & z,t '||' z,u ) ; ::_thesis: verum end; theorem Th44: :: DIRAF:44 for AS being non empty AffinStruct for S being OAffinPlane st AS = Lambda S holds for x, y, z, t being Element of AS st not x,y // z,t holds ex u being Element of AS st ( x,y // x,u & z,t // z,u ) proof let AS be non empty AffinStruct ; ::_thesis: for S being OAffinPlane st AS = Lambda S holds for x, y, z, t being Element of AS st not x,y // z,t holds ex u being Element of AS st ( x,y // x,u & z,t // z,u ) let S be OAffinPlane; ::_thesis: ( AS = Lambda S implies for x, y, z, t being Element of AS st not x,y // z,t holds ex u being Element of AS st ( x,y // x,u & z,t // z,u ) ) assume A1: AS = Lambda S ; ::_thesis: for x, y, z, t being Element of AS st not x,y // z,t holds ex u being Element of AS st ( x,y // x,u & z,t // z,u ) let x, y, z, t be Element of AS; ::_thesis: ( not x,y // z,t implies ex u being Element of AS st ( x,y // x,u & z,t // z,u ) ) reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of S by A1; assume not x,y // z,t ; ::_thesis: ex u being Element of AS st ( x,y // x,u & z,t // z,u ) then not x9,y9 '||' z9,t9 by A1, Th38; then consider u9 being Element of S such that A2: ( x9,y9 '||' x9,u9 & z9,t9 '||' z9,u9 ) by Th43; reconsider u = u9 as Element of AS by A1; ( x,y // x,u & z,t // z,u ) by A1, A2, Th38; hence ex u being Element of AS st ( x,y // x,u & z,t // z,u ) ; ::_thesis: verum end; definition let IT be non empty AffinStruct ; attrIT is 2-dimensional means :Def7: :: DIRAF:def 7 for x, y, z, t being Element of IT st not x,y // z,t holds ex u being Element of IT st ( x,y // x,u & z,t // z,u ); end; :: deftheorem Def7 defines 2-dimensional DIRAF:def_7_:_ for IT being non empty AffinStruct holds ( IT is 2-dimensional iff for x, y, z, t being Element of IT st not x,y // z,t holds ex u being Element of IT st ( x,y // x,u & z,t // z,u ) ); registration cluster non empty non trivial strict AffinSpace-like 2-dimensional for AffinStruct ; existence ex b1 being AffinSpace st ( b1 is strict & b1 is 2-dimensional ) proof set S = the OAffinPlane; reconsider AS = Lambda the OAffinPlane as AffinSpace by Th41; for x, y, z, t being Element of AS st not x,y // z,t holds ex u being Element of AS st ( x,y // x,u & z,t // z,u ) by Th44; then AS is 2-dimensional by Def7; hence ex b1 being AffinSpace st ( b1 is strict & b1 is 2-dimensional ) ; ::_thesis: verum end; end; definition mode AffinPlane is 2-dimensional AffinSpace; end; theorem :: DIRAF:45 for S being OAffinPlane holds Lambda S is AffinPlane proof let S be OAffinPlane; ::_thesis: Lambda S is AffinPlane set AS = Lambda S; for x, y, z, t being Element of (Lambda S) st not x,y // z,t holds ex u being Element of (Lambda S) st ( x,y // x,u & z,t // z,u ) by Th44; hence Lambda S is AffinPlane by Def7, Th41; ::_thesis: verum end; theorem :: DIRAF:46 for AS being non empty AffinStruct holds ( AS is AffinPlane iff ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st ( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st ( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds ex u being Element of AS st ( y,x // x,u & y,z // t,u ) ) & ( for x, y, z, t being Element of AS st not x,y // z,t holds ex u being Element of AS st ( x,y // x,u & z,t // z,u ) ) ) ) by Def6, Def7, STRUCT_0:def_10;