:: 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;