:: EUCLMETR semantic presentation

begin

definition
let IT be ( ( V42() OrtAfSp-like ) ( V42() OrtAfSp-like ) OrtAfSp) ;
attr IT is Euclidean means :: EUCLMETR:def 1
 for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ;
end;

definition
let IT be ( ( V42() OrtAfSp-like ) ( V42() OrtAfSp-like ) OrtAfSp) ;
attr IT is Pappian means :: EUCLMETR:def 2
 Af IT : ( ( ) ( ) ParOrtStr ) : ( ( strict ) ( strict ) AffinStruct ) is Pappian ;
end;

definition
let IT be ( ( V42() OrtAfSp-like ) ( V42() OrtAfSp-like ) OrtAfSp) ;
attr IT is Desarguesian means :: EUCLMETR:def 3
 Af IT : ( ( ) ( ) ParOrtStr ) : ( ( strict ) ( strict ) AffinStruct ) is Desarguesian ;
end;

definition
let IT be ( ( V42() OrtAfSp-like ) ( V42() OrtAfSp-like ) OrtAfSp) ;
attr IT is Fanoian means :: EUCLMETR:def 4
 Af IT : ( ( ) ( ) ParOrtStr ) : ( ( strict ) ( strict ) AffinStruct ) is Fanoian ;
end;

definition
let IT be ( ( V42() OrtAfSp-like ) ( V42() OrtAfSp-like ) OrtAfSp) ;
attr IT is Moufangian means :: EUCLMETR:def 5
 Af IT : ( ( ) ( ) ParOrtStr ) : ( ( strict ) ( strict ) AffinStruct ) is Moufangian ;
end;

definition
let IT be ( ( V42() OrtAfSp-like ) ( V42() OrtAfSp-like ) OrtAfSp) ;
attr IT is translation means :: EUCLMETR:def 6
 Af IT : ( ( ) ( ) ParOrtStr ) : ( ( strict ) ( strict ) AffinStruct ) is translational ;
end;

definition
let IT be ( ( V42() OrtAfSp-like ) ( V42() OrtAfSp-like ) OrtAfSp) ;
attr IT is Homogeneous means :: EUCLMETR:def 7
 for o, a, a1, b, b1, c, c1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ a1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ a1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ b1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ;
end;

theorem :: EUCLMETR:1
for MP being ( ( V42() OrtAfSp-like ) ( V42() OrtAfSp-like ) OrtAfSp)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) st not LIN a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ) ;

theorem :: EUCLMETR:2
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V1() ) set ) )
for K being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ K : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ K : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ) ;

theorem :: EUCLMETR:3
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl)
for a, b being ( ( ) ( ) Element of ( ( ) ( V1() ) set ) )
for A, K being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ K : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) or b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ K : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) & a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ A : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
K : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) // A : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ;

theorem :: EUCLMETR:4
for MP being ( ( V42() OrtAfSp-like ) ( V42() OrtAfSp-like ) OrtAfSp)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) st LIN x : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) holds
( LIN x : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & LIN y : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & LIN y : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & LIN z : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & LIN z : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ) ;

theorem :: EUCLMETR:5
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) st not LIN a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) holds
ex d being ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) st
( d : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ) ;

theorem :: EUCLMETR:6
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl)
for a, b, c, d1, d2 being ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) st not LIN a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & d1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & d1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & d2 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & d2 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) holds
d1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) = d2 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ;

theorem :: EUCLMETR:7
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & LIN a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ;

theorem :: EUCLMETR:8
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) holds
( MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is Euclidean iff MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is satisfying_3H ) ;

theorem :: EUCLMETR:9
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) holds
( MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is Homogeneous iff MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is satisfying_ODES ) ;

theorem :: EUCLMETR:10
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) holds
( MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is Pappian iff MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is satisfying_PAP ) ;

theorem :: EUCLMETR:11
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) holds
( MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is Desarguesian iff MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is satisfying_DES ) ;

theorem :: EUCLMETR:12
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) holds
( MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is Moufangian iff MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is satisfying_TDES ) ;

theorem :: EUCLMETR:13
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) holds
( MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is translation iff MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is satisfying_des ) ;

theorem :: EUCLMETR:14
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) st MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is Homogeneous holds
MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is Desarguesian ;

theorem :: EUCLMETR:15
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) st MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is Euclidean & MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is Desarguesian holds
MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is Pappian ;

theorem :: EUCLMETR:16
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl)
for o, c, c1, a, a1, a2 being ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) st not LIN o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) <> c1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ c1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ c1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) holds
a1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) = a2 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ;

theorem :: EUCLMETR:17
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl)
for o, c, c1, a being ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) st not LIN o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) holds
ex a1 being ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) st
( o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ c1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ) ;

theorem :: EUCLMETR:18
for V being ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for w, y, u, v being ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) )
for a, b being ( ( ) ( V11() V12() ) Real) st Gen w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) & 0. V : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V49(b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) <> u : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) & 0. V : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V49(b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) are_Ort_wrt w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) = (a : ( ( ) ( V11() V12() ) Real) * w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) + (b : ( ( ) ( V11() V12() ) Real) * y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) holds
ex c being ( ( ) ( V11() V12() ) Real) st
( c : ( ( ) ( V11() V12() ) Real) <> 0 : ( ( ) ( V4() V5() V6() V10() V11() V12() ) Element of K32() : ( ( ) ( V1() V4() V5() V6() ) Element of K6(K28() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) = ((c : ( ( ) ( V11() V12() ) Real) * b : ( ( ) ( V11() V12() ) Real) ) : ( ( ) ( V11() V12() ) Element of K28() : ( ( ) ( ) set ) ) * w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) + ((- (c : ( ( ) ( V11() V12() ) Real) * a : ( ( ) ( V11() V12() ) Real) ) : ( ( ) ( V11() V12() ) Element of K28() : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() ) Element of K28() : ( ( ) ( ) set ) ) * y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) ) ;

theorem :: EUCLMETR:19
for V being ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for w, y, u, v being ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) st Gen w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) & 0. V : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V49(b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) <> u : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) & 0. V : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V49(b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) are_Ort_wrt w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) holds
ex c being ( ( ) ( V11() V12() ) Real) st
for a, b being ( ( ) ( V11() V12() ) Real) holds
( (a : ( ( ) ( V11() V12() ) Real) * w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) + (b : ( ( ) ( V11() V12() ) Real) * y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) ,((c : ( ( ) ( V11() V12() ) Real) * b : ( ( ) ( V11() V12() ) Real) ) : ( ( ) ( V11() V12() ) Element of K28() : ( ( ) ( ) set ) ) * w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) + ((- (c : ( ( ) ( V11() V12() ) Real) * a : ( ( ) ( V11() V12() ) Real) ) : ( ( ) ( V11() V12() ) Element of K28() : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() ) Element of K28() : ( ( ) ( ) set ) ) * y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) are_Ort_wrt w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) & ((a : ( ( ) ( V11() V12() ) Real) * w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) + (b : ( ( ) ( V11() V12() ) Real) * y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) ,(((c : ( ( ) ( V11() V12() ) Real) * b : ( ( ) ( V11() V12() ) Real) ) : ( ( ) ( V11() V12() ) Element of K28() : ( ( ) ( ) set ) ) * w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) + ((- (c : ( ( ) ( V11() V12() ) Real) * a : ( ( ) ( V11() V12() ) Real) ) : ( ( ) ( V11() V12() ) Element of K28() : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() ) Element of K28() : ( ( ) ( ) set ) ) * y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V1() ) set ) ) are_Ort_wrt w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) ;

theorem :: EUCLMETR:20
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl)
for V being ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for w, y being ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) st Gen w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) & MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) = AMSpace (V : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( strict ) ( V42() strict ) ParOrtStr ) holds
MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is satisfying_LIN ;

theorem :: EUCLMETR:21
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl)
for o, a, a1, b, b1, c, c1 being ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ a1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ a1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) = a1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) _|_ b1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( V1() ) set ) ) ;

theorem :: EUCLMETR:22
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl)
for V being ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for w, y being ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) st Gen w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) & MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) = AMSpace (V : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( strict ) ( V42() strict ) ParOrtStr ) holds
MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is Homogeneous ;

registration
cluster V42() OrtAfSp-like OrtAfPl-like Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous for ( ( ) ( ) ParOrtStr ) ;
end;

registration
cluster V42() OrtAfSp-like Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous for ( ( ) ( ) ParOrtStr ) ;
end;

theorem :: EUCLMETR:23
for MS being ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl)
for V being ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for w, y being ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) st Gen w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) & MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) = AMSpace (V : ( ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ,w : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( V1() ) set ) ) ) : ( ( strict ) ( V42() strict ) ParOrtStr ) holds
MS : ( ( V42() OrtAfPl-like ) ( V42() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is ( ( V42() OrtAfPl-like Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous ) ( V42() OrtAfSp-like OrtAfPl-like Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous ) OrtAfPl) ;

registration
let MS be ( ( V42() OrtAfPl-like Pappian ) ( V42() OrtAfSp-like OrtAfPl-like Pappian ) OrtAfPl) ;
cluster Af MS : ( ( V42() OrtAfPl-like Pappian ) ( V42() OrtAfSp-like OrtAfPl-like Pappian ) ParOrtStr ) : ( ( strict ) ( V42() V47() strict AffinSpace-like 2-dimensional ) AffinStruct ) -> strict Pappian ;
end;

registration
let MS be ( ( V42() OrtAfPl-like Desarguesian ) ( V42() OrtAfSp-like OrtAfPl-like Desarguesian ) OrtAfPl) ;
cluster Af MS : ( ( V42() OrtAfPl-like Desarguesian ) ( V42() OrtAfSp-like OrtAfPl-like Desarguesian ) ParOrtStr ) : ( ( strict ) ( V42() V47() strict AffinSpace-like 2-dimensional ) AffinStruct ) -> strict Desarguesian ;
end;

registration
let MS be ( ( V42() OrtAfPl-like Moufangian ) ( V42() OrtAfSp-like OrtAfPl-like Moufangian ) OrtAfPl) ;
cluster Af MS : ( ( V42() OrtAfPl-like Moufangian ) ( V42() OrtAfSp-like OrtAfPl-like Moufangian ) ParOrtStr ) : ( ( strict ) ( V42() V47() strict AffinSpace-like 2-dimensional ) AffinStruct ) -> strict Moufangian ;
end;

registration
let MS be ( ( V42() OrtAfPl-like translation ) ( V42() OrtAfSp-like OrtAfPl-like translation ) OrtAfPl) ;
cluster Af MS : ( ( V42() OrtAfPl-like translation ) ( V42() OrtAfSp-like OrtAfPl-like translation ) ParOrtStr ) : ( ( strict ) ( V42() V47() strict AffinSpace-like 2-dimensional ) AffinStruct ) -> strict translational ;
end;

registration
let MS be ( ( V42() OrtAfPl-like Fanoian ) ( V42() OrtAfSp-like OrtAfPl-like Fanoian ) OrtAfPl) ;
cluster Af MS : ( ( V42() OrtAfPl-like Fanoian ) ( V42() OrtAfSp-like OrtAfPl-like Fanoian ) ParOrtStr ) : ( ( strict ) ( V42() V47() strict AffinSpace-like 2-dimensional ) AffinStruct ) -> strict Fanoian ;
end;

registration
let MS be ( ( V42() OrtAfPl-like Homogeneous ) ( V42() OrtAfSp-like OrtAfPl-like Homogeneous ) OrtAfPl) ;
cluster Af MS : ( ( V42() OrtAfPl-like Homogeneous ) ( V42() OrtAfSp-like OrtAfPl-like Homogeneous ) ParOrtStr ) : ( ( strict ) ( V42() V47() strict AffinSpace-like 2-dimensional ) AffinStruct ) -> strict Desarguesian ;
end;

registration
let MS be ( ( V42() OrtAfPl-like Euclidean Desarguesian ) ( V42() OrtAfSp-like OrtAfPl-like Euclidean Desarguesian ) OrtAfPl) ;
cluster Af MS : ( ( V42() OrtAfPl-like Euclidean Desarguesian ) ( V42() OrtAfSp-like OrtAfPl-like Euclidean Desarguesian ) ParOrtStr ) : ( ( strict ) ( V42() V47() strict AffinSpace-like 2-dimensional Desarguesian ) AffinStruct ) -> strict Pappian ;
end;

registration
let MS be ( ( V42() OrtAfSp-like Pappian ) ( V42() OrtAfSp-like Pappian ) OrtAfSp) ;
cluster Af MS : ( ( V42() OrtAfSp-like Pappian ) ( V42() OrtAfSp-like Pappian ) ParOrtStr ) : ( ( strict ) ( V42() V47() strict AffinSpace-like ) AffinStruct ) -> strict Pappian ;
end;

registration
let MS be ( ( V42() OrtAfSp-like Desarguesian ) ( V42() OrtAfSp-like Desarguesian ) OrtAfSp) ;
cluster Af MS : ( ( V42() OrtAfSp-like Desarguesian ) ( V42() OrtAfSp-like Desarguesian ) ParOrtStr ) : ( ( strict ) ( V42() V47() strict AffinSpace-like ) AffinStruct ) -> strict Desarguesian ;
end;

registration
let MS be ( ( V42() OrtAfSp-like Moufangian ) ( V42() OrtAfSp-like Moufangian ) OrtAfSp) ;
cluster Af MS : ( ( V42() OrtAfSp-like Moufangian ) ( V42() OrtAfSp-like Moufangian ) ParOrtStr ) : ( ( strict ) ( V42() V47() strict AffinSpace-like ) AffinStruct ) -> strict Moufangian ;
end;

registration
let MS be ( ( V42() OrtAfSp-like translation ) ( V42() OrtAfSp-like translation ) OrtAfSp) ;
cluster Af MS : ( ( V42() OrtAfSp-like translation ) ( V42() OrtAfSp-like translation ) ParOrtStr ) : ( ( strict ) ( V42() V47() strict AffinSpace-like ) AffinStruct ) -> strict translational ;
end;

registration
let MS be ( ( V42() OrtAfSp-like Fanoian ) ( V42() OrtAfSp-like Fanoian ) OrtAfSp) ;
cluster Af MS : ( ( V42() OrtAfSp-like Fanoian ) ( V42() OrtAfSp-like Fanoian ) ParOrtStr ) : ( ( strict ) ( V42() V47() strict AffinSpace-like ) AffinStruct ) -> strict Fanoian ;
end;