let MS be OrtAfPl; :: thesis: for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace V,w,y holds
MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl
let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y & MS = AMSpace V,w,y holds
MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl
let w, y be VECTOR of V; :: thesis: ( Gen w,y & MS = AMSpace V,w,y implies MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl )
assume A1: ( Gen w,y & MS = AMSpace V,w,y ) ; :: thesis: MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl
then reconsider MS' = AMSpace V,w,y as OrtAfPl ;
A2: MS' is satisfying_3H by A1, Th21, CONAFFM:6;
( ( for a, b being Real st (a * w) + (b * y) = 0. V holds
( a = 0 & b = 0 ) ) & ( for u being VECTOR of V ex a, b being Real st u = (a * w) + (b * y) ) ) by A1, ANALMETR:def 1;
then reconsider OAS = OASpace V as OAffinSpace by ANALOAF:38;
A3: Af MS' = Lambda OAS by ANALMETR:30;
then A4: Af MS' is Pappian by PAPDESAF:19;
A5: Af MS' is Desarguesian by A3, PAPDESAF:20;
A6: Af MS' is Moufangian by A3, PAPDESAF:22;
Af MS' is translational by A3, PAPDESAF:23;
hence MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl by A1, A2, A3, A4, A5, A6, Def2, Def3, Def4, Def5, Def6, Th8, Th23; :: thesis: verum