let x be object ; :: thesis: for V being non trivial RealLinearSpace holds
( x is Element of () iff ex u being Element of V st
( not u is zero & x = Dir u ) )

let V be non trivial RealLinearSpace; :: thesis: ( x is Element of () iff ex u being Element of V st
( not u is zero & x = Dir u ) )

now :: thesis: ( x is Element of () implies ex y being Element of V st
( not y is zero & x = Dir y ) )
assume A1: x is Element of () ; :: thesis: ex y being Element of V st
( not y is zero & x = Dir y )

A2: ex Y being Subset-Family of () st
( Y = Class & ProjectivePoints V = Y ) by Def5;
then reconsider x9 = x as Subset of () by ;
consider y being object such that
A3: y in NonZero V and
A4: x9 = Class (,y) by ;
A5: y <> 0. V by ;
reconsider y = y as Element of V by A3;
take y = y; :: thesis: ( not y is zero & x = Dir y )
thus not y is zero by A5; :: thesis: x = Dir y
thus x = Dir y by A4; :: thesis: verum
end;
hence ( x is Element of () iff ex u being Element of V st
( not u is zero & x = Dir u ) ) by Th21; :: thesis: verum