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

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