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:37;
reconsider X = OASpace V as OAffinSpace by A1, ANALOAF:38;
take Lambda X ; :: thesis: ( Lambda X is strict & Lambda X is Fanoian & Lambda X is Pappian & Lambda X is Desarguesian & Lambda X is Moufangian & Lambda X is translational )
thus ( Lambda X is strict & Lambda X is Fanoian & Lambda X is Pappian & Lambda X is Desarguesian & Lambda X is Moufangian & Lambda X is translational ) by Th19, Th20, Th22, Th23, Th24; :: thesis: verum