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 that
A1: Gen w,y and
A2: MS = AMSpace (V,w,y) ; :: thesis: MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl
reconsider MS9 = AMSpace (V,w,y) as OrtAfPl by A2;
A3: MS9 is satisfying_3H by A1, Th20, CONAFFM:6;
for a, b being Real st (a * w) + (b * y) = 0. V holds
( a = 0 & b = 0 ) by A1, ANALMETR:def 1;
then reconsider OAS = OASpace V as OAffinSpace by ANALOAF:26;
A4: AffinStruct(# the carrier of MS9, the CONGR of MS9 #) = Lambda OAS by ANALMETR:20;
then A5: ( AffinStruct(# the carrier of MS9, the CONGR of MS9 #) is Moufangian & AffinStruct(# the carrier of MS9, the CONGR of MS9 #) is translational ) by PAPDESAF:16, PAPDESAF:17;
( AffinStruct(# the carrier of MS9, the CONGR of MS9 #) is Pappian & AffinStruct(# the carrier of MS9, the CONGR of MS9 #) is Desarguesian ) by A4, PAPDESAF:13, PAPDESAF:14;
hence MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl by A1, A2, A3, A4, A5, Def2, Def3, Def4, Def5, Def6, Th8, Th22; :: thesis: verum