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 Th22, Th23;
( Lambda X is Pappian & Lambda X is Desarguesian ) by Th14, Th17, Th19;
hence ( X is Pappian & X is Desarguesian & X is Moufangian & X is translation ) by A2, Def11, Def12, Def13, Def14; :: thesis: verum