:: PAPDESAF semantic presentation

begin

registration
let OAS be ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) ;
cluster Lambda OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) AffinStruct ) : ( ( strict ) ( V52() strict ) AffinStruct ) -> non trivial strict AffinSpace-like ;
end;

registration
let OAS be ( ( non trivial OAffinSpace-like 2-dimensional ) ( V52() non trivial OAffinSpace-like 2-dimensional ) OAffinPlane) ;
cluster Lambda OAS : ( ( non trivial OAffinSpace-like 2-dimensional ) ( V52() non trivial OAffinSpace-like 2-dimensional ) AffinStruct ) : ( ( strict ) ( V52() non trivial strict AffinSpace-like ) AffinStruct ) -> strict 2-dimensional ;
end;

theorem :: PAPDESAF:1
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace)
for x being ( ( ) ( ) set ) holds
( ( x : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) implies x : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) & ( x : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) implies x : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) & ( x : ( ( ) ( ) set ) is ( ( ) ( ) Subset of ) implies x : ( ( ) ( ) set ) is ( ( ) ( ) Subset of ) ) & ( x : ( ( ) ( ) set ) is ( ( ) ( ) Subset of ) implies x : ( ( ) ( ) set ) is ( ( ) ( ) Subset of ) ) ) ;

theorem :: PAPDESAF:2
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) )
for a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) = a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) = b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) = c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
( LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) iff LIN a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PAPDESAF:3
for V being ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( ) set ) ) iff x : ( ( ) ( ) set ) is ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ;

theorem :: PAPDESAF:4
for V being ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) st OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) = OASpace V : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( strict ) ( strict ) AffinStruct ) holds
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) )
for u, v, w, y being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) = u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) = v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) = w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) = y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) iff u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) '||' w : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) ;

theorem :: PAPDESAF:5
for V being ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) st OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) = OASpace V : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( strict ) ( strict ) AffinStruct ) holds
ex u, v being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) st
for a, b being ( ( ) ( V1() V14() V15() ) Real) st (a : ( ( ) ( V1() V14() V15() ) Real) * u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) + (b : ( ( ) ( V1() V14() V15() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) = 0. V : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V59(b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) holds
( a : ( ( ) ( V1() V14() V15() ) Real) = 0 : ( ( ) ( V1() V13() V14() V15() V16() V17() V18() V19() V20() V21() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2(K11(REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ) : ( ( ) ( ) set ) )) )) & b : ( ( ) ( V1() V14() V15() ) Real) = 0 : ( ( ) ( V1() V13() V14() V15() V16() V17() V18() V19() V20() V21() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2(K11(REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ) : ( ( ) ( ) set ) )) )) ) ;

definition
let AS be ( ( non trivial AffinSpace-like ) ( V52() non trivial AffinSpace-like ) AffinSpace) ;
redefine attr AS is Fanoian means :: PAPDESAF:def 1
 for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let IT be ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) ;
attr IT is Pappian means :: PAPDESAF:def 2
 Lambda IT : ( ( V45() ) ( V45() ) set ) : ( ( strict ) ( strict ) AffinStruct ) is Pappian ;
attr IT is Desarguesian means :: PAPDESAF:def 3
 Lambda IT : ( ( V45() ) ( V45() ) set ) : ( ( strict ) ( strict ) AffinStruct ) is Desarguesian ;
attr IT is Moufangian means :: PAPDESAF:def 4
 Lambda IT : ( ( V45() ) ( V45() ) set ) : ( ( strict ) ( strict ) AffinStruct ) is Moufangian ;
attr IT is translation means :: PAPDESAF:def 5
 Lambda IT : ( ( V45() ) ( V45() ) set ) : ( ( strict ) ( strict ) AffinStruct ) is translational ;
end;

definition
let OAS be ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) ;
attr OAS is satisfying_DES means :: PAPDESAF:def 6
 for o, a, b, c, a1, b1, c1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let OAS be ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) ;
attr OAS is satisfying_DES_1 means :: PAPDESAF:def 7
 for o, a, b, c, a1, b1, c1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

theorem :: PAPDESAF:6
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) st OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) is satisfying_DES_1 holds
OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) is satisfying_DES ;

theorem :: PAPDESAF:7
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace)
for o, a, b, a9, b9 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
( b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PAPDESAF:8
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace)
for o, a, b, a9, b9 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
( o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PAPDESAF:9
for OAP being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) st OAP : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) is satisfying_DES_1 holds
Lambda OAP : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) : ( ( strict ) ( V52() non trivial strict AffinSpace-like ) AffinStruct ) is Desarguesian ;

theorem :: PAPDESAF:10
for V being ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for o, u, v, u1, v1 being ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) )
for r being ( ( ) ( V1() V14() V15() ) Real) st o : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) = r : ( ( ) ( V1() V14() V15() ) Real) * (u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) - o : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) & r : ( ( ) ( V1() V14() V15() ) Real) <> 0 : ( ( ) ( V1() V13() V14() V15() V16() V17() V18() V19() V20() V21() ) M3( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) , NAT : ( ( ) ( V16() V17() V18() V19() V20() V21() V22() ) M2(K11(REAL : ( ( ) ( V16() V17() V18() V22() ) set ) ) : ( ( ) ( ) set ) )) )) & o : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) '||' o : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & not o : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) '||' o : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) '||' u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ,v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) holds
( v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) + (((- r : ( ( ) ( V1() V14() V15() ) Real) ) : ( ( ) ( V1() V14() V15() ) M2( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) )) ") : ( ( ) ( V1() V14() V15() ) M2( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) )) * (v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) & v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) = o : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) + (((- r : ( ( ) ( V1() V14() V15() ) Real) ) : ( ( ) ( V1() V14() V15() ) M2( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) )) ") : ( ( ) ( V1() V14() V15() ) M2( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) )) * (v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) - o : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) & v : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) = (- r : ( ( ) ( V1() V14() V15() ) Real) ) : ( ( ) ( V1() V14() V15() ) M2( REAL : ( ( ) ( V16() V17() V18() V22() ) set ) )) * (v1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) - u1 : ( ( ) ( ) VECTOR of ( ( ) ( V4() ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V4() ) set ) )) ) ;

theorem :: PAPDESAF:11
for V being ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) st OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) = OASpace V : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( strict ) ( strict ) AffinStruct ) holds
OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) is satisfying_DES_1 ;

theorem :: PAPDESAF:12
for V being ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) st OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) = OASpace V : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( strict ) ( strict ) AffinStruct ) holds
( OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) is satisfying_DES_1 & OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) is satisfying_DES ) ;

theorem :: PAPDESAF:13
for V being ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) st OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) = OASpace V : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( strict ) ( strict ) AffinStruct ) holds
Lambda OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) : ( ( strict ) ( V52() non trivial strict AffinSpace-like ) AffinStruct ) is Pappian ;

theorem :: PAPDESAF:14
for V being ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) st OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) = OASpace V : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( strict ) ( strict ) AffinStruct ) holds
Lambda OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) : ( ( strict ) ( V52() non trivial strict AffinSpace-like ) AffinStruct ) is Desarguesian ;

theorem :: PAPDESAF:15
for AS being ( ( non trivial AffinSpace-like ) ( V52() non trivial AffinSpace-like ) AffinSpace) st AS : ( ( non trivial AffinSpace-like ) ( V52() non trivial AffinSpace-like ) AffinSpace) is Desarguesian holds
AS : ( ( non trivial AffinSpace-like ) ( V52() non trivial AffinSpace-like ) AffinSpace) is Moufangian ;

theorem :: PAPDESAF:16
for V being ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) st OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) = OASpace V : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( strict ) ( strict ) AffinStruct ) holds
Lambda OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) : ( ( strict ) ( V52() non trivial strict AffinSpace-like ) AffinStruct ) is Moufangian ;

theorem :: PAPDESAF:17
for V being ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) st OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) = OASpace V : ( ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( strict ) ( strict ) AffinStruct ) holds
Lambda OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) : ( ( strict ) ( V52() non trivial strict AffinSpace-like ) AffinStruct ) is translational ;

theorem :: PAPDESAF:18
for OAS being ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) holds Lambda OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) : ( ( strict ) ( V52() non trivial strict AffinSpace-like ) AffinStruct ) is Fanoian ;

registration
cluster V52() non trivial OAffinSpace-like Pappian Desarguesian Moufangian translation for ( ( ) ( ) AffinStruct ) ;
end;

registration
cluster V52() non trivial strict AffinSpace-like 2-dimensional Pappian Desarguesian Moufangian translational Fanoian for ( ( ) ( ) AffinStruct ) ;
end;

registration
cluster V52() non trivial strict AffinSpace-like Pappian Desarguesian Moufangian translational Fanoian for ( ( ) ( ) AffinStruct ) ;
end;

registration
let OAS be ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) OAffinSpace) ;
cluster Lambda OAS : ( ( non trivial OAffinSpace-like ) ( V52() non trivial OAffinSpace-like ) AffinStruct ) : ( ( strict ) ( V52() non trivial strict AffinSpace-like ) AffinStruct ) -> strict Fanoian ;
end;

registration
let OAS be ( ( non trivial OAffinSpace-like Pappian ) ( V52() non trivial OAffinSpace-like Pappian ) OAffinSpace) ;
cluster Lambda OAS : ( ( non trivial OAffinSpace-like Pappian ) ( V52() non trivial OAffinSpace-like Pappian ) AffinStruct ) : ( ( strict ) ( V52() non trivial strict AffinSpace-like Fanoian ) AffinStruct ) -> strict Pappian ;
end;

registration
let OAS be ( ( non trivial OAffinSpace-like Desarguesian ) ( V52() non trivial OAffinSpace-like Desarguesian ) OAffinSpace) ;
cluster Lambda OAS : ( ( non trivial OAffinSpace-like Desarguesian ) ( V52() non trivial OAffinSpace-like Desarguesian ) AffinStruct ) : ( ( strict ) ( V52() non trivial strict AffinSpace-like Fanoian ) AffinStruct ) -> strict Desarguesian ;
end;

registration
let OAS be ( ( non trivial OAffinSpace-like Moufangian ) ( V52() non trivial OAffinSpace-like Moufangian ) OAffinSpace) ;
cluster Lambda OAS : ( ( non trivial OAffinSpace-like Moufangian ) ( V52() non trivial OAffinSpace-like Moufangian ) AffinStruct ) : ( ( strict ) ( V52() non trivial strict AffinSpace-like Fanoian ) AffinStruct ) -> strict Moufangian ;
end;

registration
let OAS be ( ( non trivial OAffinSpace-like translation ) ( V52() non trivial OAffinSpace-like translation ) OAffinSpace) ;
cluster Lambda OAS : ( ( non trivial OAffinSpace-like translation ) ( V52() non trivial OAffinSpace-like translation ) AffinStruct ) : ( ( strict ) ( V52() non trivial strict AffinSpace-like Fanoian ) AffinStruct ) -> strict translational ;
end;