consider V being RealLinearSpace such that
A1: ex w, y being VECTOR of V st Gen w,y by ANALMETR:7;
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:46;
take MS ; :: thesis: ( MS is Euclidean & MS is Pappian & MS is Desarguesian & MS is Homogeneous & MS is translation & MS is Fanoian & MS is Moufangian )
A3: MS is satisfying_3H by A2, 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 A2, ANALMETR:def 1;
then reconsider OAS = OASpace V as OAffinSpace by ANALOAF:38;
A4: Af MS = Lambda OAS by ANALMETR:30;
then A5: Af MS is Pappian by PAPDESAF:19;
A6: Af MS is Desarguesian by A4, PAPDESAF:20;
A7: Af MS is Moufangian by A4, PAPDESAF:22;
Af MS is translational by A4, PAPDESAF:23;
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, A6, A7, Def2, Def3, Def4, Def5, Def6, Th8, Th23; :: thesis: verum