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 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 Th13, Th14, Th16, Th17, Th18; :: thesis: verum