consider V being RealLinearSpace such that
A1: ex u, v being VECTOR of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) by FUNCSDOM:23;
reconsider OAS = OASpace V as OAffinPlane by A1, ANALOAF:28;
take X = Lambda OAS; :: thesis: ( X is strict & X is Fanoian & X is Pappian & X is Desarguesian & X is Moufangian & X is translational )
A2: X is Pappian by Th13;
then X is Moufangian by AFF_2:11, AFF_2:12;
hence ( X is strict & X is Fanoian & X is Pappian & X is Desarguesian & X is Moufangian & X is translational ) by A2, Th18, AFF_2:11, AFF_2:14; :: thesis: verum