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 ) by FUNCSDOM:23;
reconsider X = OASpace V as OAffinSpace by A1, ANALOAF:26;
take X ; :: thesis: ( X is Pappian & X is Desarguesian & X is Moufangian & X is translation )
set AS = Lambda X;
A2: ( Lambda X is Moufangian & Lambda X is translational ) by Th16, Th17;
( Lambda X is Pappian & Lambda X is Desarguesian ) by Th9, Th11, Th13;
hence ( X is Pappian & X is Desarguesian & X is Moufangian & X is translation ) by A2, Def2, Def3, Def4, Def5; :: thesis: verum