SEMI_AF1

:: SEMI_AF1 semantic presentation

begin

definition

let IT be ( ( non empty ) ( non empty ) AffinStruct ) ;

attr IT is Semi_Affine_Space-like means :: SEMI_AF1:def 1
( ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) & ( for a, b, p, q, r, s being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) & not for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & ( for a, b, p being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ) & ( for o, a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex p being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
for b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & ex d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) implies ( o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ) ) ) & ( for o, a, a9, b, b9, c, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) & ( for a, a9, b, b9, c, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) & ( for a1, a2, a3, b1, b2, b3 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) & ( for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) );

end;

registration

cluster non empty Semi_Affine_Space-like for ( ( ) ( ) AffinStruct ) ;

end;

definition

mode Semi_Affine_Space is ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) AffinStruct ) ;

end;

theorem :: SEMI_AF1:1

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:2

theorem :: SEMI_AF1:3

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:4

theorem :: SEMI_AF1:5

theorem :: SEMI_AF1:6

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:7

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:8

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, p, q, r, s being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:9

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:10

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, p, q being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:11

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, x, c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:12

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, p, q being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
not p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:13

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for p, q being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
ex r being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:14

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:15

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d, p, q, r, s being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
not p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:16

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, p, q, r being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
not p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:17

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, p, r being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:18

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for p, q, r1, r2 being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
r1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = r2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:19

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, p, q, r1, r2 being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
r1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = r2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:20

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st ( a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) or c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) or ( a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) or ( a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:21

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st ( a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) or b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

definition

let SAS be ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space) ;
let a, b, c be ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

pred a,b,c is_collinear means :: SEMI_AF1:def 2
a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) // a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ;

end;

theorem :: SEMI_AF1:22

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a1, a2, a3 being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear holds
( a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ) ;

theorem :: SEMI_AF1:23

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, p, q, r being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
not p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ;

theorem :: SEMI_AF1:24

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st ( a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) or b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) or c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ;

theorem :: SEMI_AF1:25

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for p, q being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
ex r being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ;

theorem :: SEMI_AF1:26

theorem :: SEMI_AF1:27

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ;

theorem :: SEMI_AF1:28

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d, x being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear holds
not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ;

theorem :: SEMI_AF1:29

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for o, a, b, x being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear holds
o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:30

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for o, a, b, a9, b9 being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:31

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d, p1, p2 being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear holds
p1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = p2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:32

theorem :: SEMI_AF1:33

theorem :: SEMI_AF1:34

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for o, a, c, b, d1, d2 being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
d1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = d2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:35

definition

let SAS be ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space) ;
let a, b, c, d be ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

pred parallelogram a,b,c,d means :: SEMI_AF1:def 3
( not a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) is_collinear & a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) // c : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,d : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) & a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) // b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,d : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) );

end;

theorem :: SEMI_AF1:36

theorem :: SEMI_AF1:37

theorem :: SEMI_AF1:38

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a1, a2, a3, a4 being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st parallelogram a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( not a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & not a4 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ) ;

theorem :: SEMI_AF1:39

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d, x being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( not parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) or not a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear or not c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ) ;

theorem :: SEMI_AF1:40

theorem :: SEMI_AF1:41

theorem :: SEMI_AF1:42

theorem :: SEMI_AF1:43

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & parallelogram c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & parallelogram b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & parallelogram c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & parallelogram d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & parallelogram b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:44

theorem :: SEMI_AF1:45

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d1, d2 being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
d1 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = d2 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:46

theorem :: SEMI_AF1:47

theorem :: SEMI_AF1:48

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
ex c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:49

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, a9, b, b9, c, c9 being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:50

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for b, b9, c, a, a9, c9 being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
parallelogram b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:51

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
parallelogram b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:52

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, a9, b, b9, c, c9, d, d9 being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & parallelogram b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d9 : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:53

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
ex b, c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st parallelogram a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

definition

let SAS be ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space) ;
let a, b, r, s be ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

pred congr a,b,r,s means :: SEMI_AF1:def 4
( ( a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) & r : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) = s : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ) or ex p, q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( parallelogram p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) & parallelogram p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,s : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ) );

end;

theorem :: SEMI_AF1:54

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:55

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:56

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:57

theorem :: SEMI_AF1:58

theorem :: SEMI_AF1:59

theorem :: SEMI_AF1:60

theorem :: SEMI_AF1:61

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d, r, s being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & parallelogram r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
parallelogram r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:62

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, x, y being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:63

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ex d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:64

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:65

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for r, s, a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:66

theorem :: SEMI_AF1:67

theorem :: SEMI_AF1:68

theorem :: SEMI_AF1:69

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( congr c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:70

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, p, q, c, s being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:71

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for b, a, p, q, c, r being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
congr b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:72

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, o, p, b, q being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:73

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for b, a, p, q, c, r being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:74

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, o, p, b, q being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & congr b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

definition

let SAS be ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space) ;
let a, b, o be ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

func sum (a,b,o) -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) means :: SEMI_AF1:def 5
congr o : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,it : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ;

end;

definition

let SAS be ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space) ;
let a, o be ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

func opposite (a,o) -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) means :: SEMI_AF1:def 6
sum (a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,it : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,o : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = o : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ;

end;

definition

let SAS be ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space) ;
let a, b, o be ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

func diff (a,b,o) -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: SEMI_AF1:def 7
sum (a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,(opposite (b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,o : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,o : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

end;

theorem :: SEMI_AF1:75

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, o being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds sum (a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:76

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, o being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ex x being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st sum (a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:77

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, o, c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds sum ((sum (a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = sum (a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,(sum (b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:78

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, o being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds sum (a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = sum (b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:79

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, o being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st sum (a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:80

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, x, o, y being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st sum (a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = sum (a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:81

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, o being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds congr a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) , opposite (a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:82

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, o, b being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st opposite (a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = opposite (b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:83

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, o being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // opposite (a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) , opposite (b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:84

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for o being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds opposite (o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:85

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for p, q, r, o being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // sum (p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) , sum (q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:86

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for p, q, r, s, o being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // sum (p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) , sum (q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:87

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, o being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( diff (a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) iff a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:88

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for o, b, a being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) , diff (b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:89

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for o, b, a, d, c being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) , diff (b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) , diff (d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear iff a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

definition

let SAS be ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space) ;
let a, b, c, d, o be ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

pred trap a,b,c,d,o means :: SEMI_AF1:def 8
( not o : ( ( V12() ) ( V12() ) M2(K24(K25(b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) is_collinear & o : ( ( V12() ) ( V12() ) M2(K24(K25(b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) is_collinear & o : ( ( V12() ) ( V12() ) M2(K24(K25(b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,d : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) is_collinear & a : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) // b : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,d : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) );

end;

definition

let SAS be ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space) ;
let o, p be ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

pred qtrap o,p means :: SEMI_AF1:def 9
for b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( o : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,p : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear implies ( o : ( ( ) ( ) M2(K24(K25(K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(SAS : ( ( ) ( ) AffinStruct ) ,SAS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & p : ( ( ) ( ) M2( the U1 of SAS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) );

end;

theorem :: SEMI_AF1:90

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d, o being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
( o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:91

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, x, o, y being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:92

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for o, a, b being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear holds
trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:93

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d, o being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
trap c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:94

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:95

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for o, b, a, c, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
not o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear ;

theorem :: SEMI_AF1:96

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for o, b, a, c, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
trap b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:97

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) = d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:98

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, p, b, q, o, c, r being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:99

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, p, b, q, o, c, r being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear holds
trap b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:100

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for a, p, b, q, o, c, r, d, s being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & trap a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & trap b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;

theorem :: SEMI_AF1:101

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for o, a being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ex p being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st
( o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & qtrap o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:102

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space) ex x, y, z being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> z : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) <> x : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:103

theorem :: SEMI_AF1:104

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for o, p being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st qtrap o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
ex q being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st
( not o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & qtrap o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ) ;

theorem :: SEMI_AF1:105

for SAS being ( ( non empty Semi_Affine_Space-like ) ( non empty Semi_Affine_Space-like ) Semi_Affine_Space)
for o, p, c, b being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st not o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) is_collinear & qtrap o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) holds
ex d being ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) st trap p : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() ) set ) ) ;