let x be object ; :: thesis: for V being non trivial RealLinearSpace holds
( x is Element of (ProjectiveSpace V) 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 (ProjectiveSpace V) iff ex u being Element of V st
( not u is zero & x = Dir u ) )
now :: thesis: ( x is Element of (ProjectiveSpace V) implies ex y being Element of V st
( not y is zero & x = Dir y ) )
assume A1: x is Element of (ProjectiveSpace V) ; :: thesis: ex y being Element of V st
( not y is zero & x = Dir y )
A2: ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & ProjectivePoints V = Y ) by Def5;
then reconsider x9 = x as Subset of (NonZero V) by A1, TARSKI:def 3;
consider y being object such that
A3: y in NonZero V and
A4: x9 = Class ((Proportionality_as_EqRel_of V),y) by A1, A2, EQREL_1:def 3;
A5: y <> 0. V by A3, ZFMISC_1:56;
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 (ProjectiveSpace V) iff ex u being Element of V st
( not u is zero & x = Dir u ) ) by Th21; :: thesis: verum