:: DIRAF semantic presentation

begin

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let R be ( ( ) ( V7() V10([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) V11([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) ) Relation of ) ;
func lambda R -> ( ( ) ( V7() V10([:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ) V11([:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ) ) Relation of ) means :: DIRAF:def 1
 for a, b, c, d being ( ( ) ( ) Element of X : ( ( ) ( ) AffinStruct ) ) holds
( [[a : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ) ,[c : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ) ] : ( ( ) ( ) Element of [:[:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ,[:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) in it : ( ( ) ( ) Element of X : ( ( ) ( ) AffinStruct ) ) iff ( [[a : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ) ,[c : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ) ] : ( ( ) ( ) Element of [:[:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ,[:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) in R : ( ( ) ( V7() V10([:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ) V11([:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ) ) Element of bool [:[:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ,[:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) or [[a : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ) ,[d : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ) ] : ( ( ) ( ) Element of [:[:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ,[:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) in R : ( ( ) ( V7() V10([:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ) V11([:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ) ) Element of bool [:[:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) ,[:X : ( ( ) ( ) AffinStruct ) ,X : ( ( ) ( ) AffinStruct ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) );
end;

definition
let S be ( ( non empty ) ( non empty ) AffinStruct ) ;
func Lambda S -> ( ( strict ) ( strict ) AffinStruct ) equals :: DIRAF:def 2
 AffinStruct(# the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) ,(lambda the CONGR of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( V7() V10([: the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V11([: the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,[: the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V7() V10([: the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V11([: the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) ) Relation of ) #) : ( ( strict ) ( strict ) AffinStruct ) ;
end;

registration
let S be ( ( non empty ) ( non empty ) AffinStruct ) ;
cluster Lambda S : ( ( non empty ) ( non empty ) AffinStruct ) : ( ( strict ) ( strict ) AffinStruct ) -> non empty strict ;
end;

theorem :: DIRAF:1
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:2
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: DIRAF:3
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for z, t, x, y, u, w being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:4
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: DIRAF:5
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & not x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:6
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) iff ( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ) ;

definition
let S be ( ( non empty ) ( non empty ) AffinStruct ) ;
let a, b, c be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
pred Mid a,b,c means :: DIRAF:def 3
a : ( ( ) ( ) set ) ,b : ( ( ) ( ) Element of S : ( ( V34() ) ( V34() ) set ) ) // b : ( ( ) ( ) Element of S : ( ( V34() ) ( V34() ) set ) ) ,c : ( ( ) ( ) Element of S : ( ( V34() ) ( V34() ) set ) ) ;
end;

theorem :: DIRAF:7
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) iff ( Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ) ;

theorem :: DIRAF:8
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st Mid a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:9
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st Mid a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
Mid c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:10
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: DIRAF:11
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st Mid a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & Mid a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
Mid b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:12
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for b, c, a, d being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & Mid a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & Mid b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
Mid a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:13
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ex z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st
( Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: DIRAF:14
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & Mid y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:15
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & not Mid y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
Mid y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:16
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & not Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:17
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, t, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & not Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
Mid x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

definition
let S be ( ( non empty ) ( non empty ) AffinStruct ) ;
let a, b, c, d be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
pred a,b '||' c,d means :: DIRAF:def 4
( a : ( ( ) ( ) set ) ,b : ( ( ) ( ) Element of S : ( ( V34() ) ( V34() ) set ) ) // c : ( ( ) ( ) Element of S : ( ( V34() ) ( V34() ) set ) ) ,d : ( ( ) ( ) Element of S : ( ( V34() ) ( V34() ) set ) ) or a : ( ( ) ( ) set ) ,b : ( ( ) ( ) Element of S : ( ( V34() ) ( V34() ) set ) ) // d : ( ( ) ( ) Element of S : ( ( V34() ) ( V34() ) set ) ) ,c : ( ( ) ( ) Element of S : ( ( V34() ) ( V34() ) set ) ) );
end;

theorem :: DIRAF:18
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) iff [[a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) , the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( non empty ) set ) ) ,[c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) , the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [:[: the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) , the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( non empty ) set ) ,[: the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) , the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) in lambda the CONGR of S : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( V7() V10([: the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) , the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( non empty ) set ) ) V11([: the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) , the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) , the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( non empty ) set ) ,[: the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) , the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V7() V10([: the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) , the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( non empty ) set ) ) V11([: the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) , the carrier of b1 : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( non empty ) set ) ) ) Relation of ) ) ;

theorem :: DIRAF:19
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: DIRAF:20
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: DIRAF:21
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:22
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: DIRAF:23
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for a, b, x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & ( ( a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) or ( a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) or ( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) or ( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:24
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) holds
not for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:25
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, z, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ex t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: DIRAF:26
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ex t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: DIRAF:27
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for z, x, t, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
ex u being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st
( y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

definition
let S be ( ( non empty ) ( non empty ) AffinStruct ) ;
let a, b, c be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
pred LIN a,b,c means :: DIRAF:def 5
a : ( ( ) ( ) set ) ,b : ( ( ) ( ) Element of S : ( ( V34() ) ( V34() ) set ) ) '||' a : ( ( ) ( ) set ) ,c : ( ( ) ( ) Element of S : ( ( V34() ) ( V34() ) set ) ) ;
end;

notation
let S be ( ( non empty ) ( non empty ) AffinStruct ) ;
let a, b, c be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
synonym a,b,c is_collinear for LIN a,b,c;
end;

theorem :: DIRAF:28
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st Mid a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear ;

theorem :: DIRAF:29
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( not a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear or Mid a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or Mid b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or Mid a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: DIRAF:30
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear & y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear & y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear & z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear & z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear ) ;

theorem :: DIRAF:31
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear ) ;

theorem :: DIRAF:32
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z, t, u being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear holds
z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear ;

theorem :: DIRAF:33
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear ;

theorem :: DIRAF:34
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear holds
x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: DIRAF:35
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for u, z, x, y, w being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear & u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear holds
x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear ;

theorem :: DIRAF:36
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) holds
not for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear ;

theorem :: DIRAF:37
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
ex z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st not x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is_collinear ;

theorem :: DIRAF:38
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for AS being ( ( non empty ) ( non empty ) AffinStruct ) st AS : ( ( non empty ) ( non empty ) AffinStruct ) = Lambda S : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( strict ) ( non empty strict ) AffinStruct ) holds
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) )
for a9, b9, c9, d9 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = a9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = c9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = d9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: DIRAF:39
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace)
for AS being ( ( non empty ) ( non empty ) AffinStruct ) st AS : ( ( non empty ) ( non empty ) AffinStruct ) = Lambda S : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( strict ) ( non empty strict ) AffinStruct ) holds
( ex x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for x, y, z, t, u, w being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) & not for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex u being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) ;

definition
let IT be ( ( non empty ) ( non empty ) AffinStruct ) ;
attr IT is AffinSpace-like means :: DIRAF:def 6
( ( for x, y, z, t, u, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) & not for x, y, z being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for x, y, z being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex t being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for x, y, z being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex t being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex u being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) );
end;

registration
cluster non empty non trivial strict AffinSpace-like for ( ( ) ( ) AffinStruct ) ;
end;

definition
mode AffinSpace is ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinStruct ) ;
end;

theorem :: DIRAF:40
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) holds
( ex x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & ( for x, y, z, t, u, w being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) implies z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) implies y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ) ) & not for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & ( for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ex t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ) & ( for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ex t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ) & ( for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
ex u being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st
( y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ) ) ;

theorem :: DIRAF:41
for S being ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) holds Lambda S : ( ( non trivial OAffinSpace-like ) ( non empty non trivial OAffinSpace-like ) OAffinSpace) : ( ( strict ) ( non empty strict ) AffinStruct ) is ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;

theorem :: DIRAF:42
for AS being ( ( non empty ) ( non empty ) AffinStruct ) holds
( ( ex x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for x, y, z, t, u, w being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) & not for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex u being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) iff AS : ( ( non empty ) ( non empty ) AffinStruct ) is ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) ;

theorem :: DIRAF:43
for S being ( ( non trivial OAffinSpace-like 2-dimensional ) ( non empty non trivial OAffinSpace-like 2-dimensional ) OAffinPlane)
for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st not x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
ex u being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) '||' z : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: DIRAF:44
for AS being ( ( non empty ) ( non empty ) AffinStruct )
for S being ( ( non trivial OAffinSpace-like 2-dimensional ) ( non empty non trivial OAffinSpace-like 2-dimensional ) OAffinPlane) st AS : ( ( non empty ) ( non empty ) AffinStruct ) = Lambda S : ( ( non trivial OAffinSpace-like 2-dimensional ) ( non empty non trivial OAffinSpace-like 2-dimensional ) OAffinPlane) : ( ( strict ) ( non empty strict ) AffinStruct ) holds
for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex u being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

definition
let IT be ( ( non empty ) ( non empty ) AffinStruct ) ;
attr IT is 2-dimensional means :: DIRAF:def 7
 for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex u being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) );
end;

registration
cluster non empty non trivial strict AffinSpace-like 2-dimensional for ( ( ) ( ) AffinStruct ) ;
end;

definition
mode AffinPlane is ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinSpace) ;
end;

theorem :: DIRAF:45
for S being ( ( non trivial OAffinSpace-like 2-dimensional ) ( non empty non trivial OAffinSpace-like 2-dimensional ) OAffinPlane) holds Lambda S : ( ( non trivial OAffinSpace-like 2-dimensional ) ( non empty non trivial OAffinSpace-like 2-dimensional ) OAffinPlane) : ( ( strict ) ( non empty strict ) AffinStruct ) is ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinPlane) ;

theorem :: DIRAF:46
for AS being ( ( non empty ) ( non empty ) AffinStruct ) holds
( AS : ( ( non empty ) ( non empty ) AffinStruct ) is ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinPlane) iff ( ex x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for x, y, z, t, u, w being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) & not for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex u being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex u being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) ) ;