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 ) )

( not u is zero & x = Dir u ) ) by Th21; :: thesis: verum

( 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 ) )

hence
( x is Element of (ProjectiveSpace V) iff ex u 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;( 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

( not u is zero & x = Dir u ) ) by Th21; :: thesis: verum