consider V being RealLinearSpace such that
A1:
ex w, y being VECTOR of V st Gen w,y
by ANALMETR:3;
consider w, y being VECTOR of V such that
A2:
Gen w,y
by A1;
reconsider MS = AMSpace (V,w,y) as OrtAfPl by A2, ANALMETR:34;
A3:
MS is satisfying_3H
by A2, Th20, CONAFFM:6;
for a, b being Real st (a * w) + (b * y) = 0. V holds
( a = 0 & b = 0 )
by A2, ANALMETR:def 1;
then reconsider OAS = OASpace V as OAffinSpace by ANALOAF:26;
take
MS
; ( MS is Euclidean & MS is Pappian & MS is Desarguesian & MS is Homogeneous & MS is translation & MS is Fanoian & MS is Moufangian )
A4:
AffinStruct(# the carrier of MS, the CONGR of MS #) = Lambda OAS
by ANALMETR:20;
then A5:
( AffinStruct(# the carrier of MS, the CONGR of MS #) is Moufangian & AffinStruct(# the carrier of MS, the CONGR of MS #) is translational )
by PAPDESAF:16, PAPDESAF:17;
( AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian & AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian )
by A4, PAPDESAF:13, PAPDESAF:14;
hence
( MS is Euclidean & MS is Pappian & MS is Desarguesian & MS is Homogeneous & MS is translation & MS is Fanoian & MS is Moufangian )
by A2, A3, A4, A5, Th8, Th22; verum