let V be non trivial RealLinearSpace; :: thesis: for p being Element of V st not p is zero holds

Dir p is Element of ProjectivePoints V

let p be Element of V; :: thesis: ( not p is zero implies Dir p is Element of ProjectivePoints V )

assume not p is zero ; :: thesis: Dir p is Element of ProjectivePoints V

then p in NonZero V by STRUCT_0:1;

then Dir p in Class (Proportionality_as_EqRel_of V) by EQREL_1:def 3;

hence Dir p is Element of ProjectivePoints V by Def5; :: thesis: verum

Dir p is Element of ProjectivePoints V

let p be Element of V; :: thesis: ( not p is zero implies Dir p is Element of ProjectivePoints V )

assume not p is zero ; :: thesis: Dir p is Element of ProjectivePoints V

then p in NonZero V by STRUCT_0:1;

then Dir p in Class (Proportionality_as_EqRel_of V) by EQREL_1:def 3;

hence Dir p is Element of ProjectivePoints V by Def5; :: thesis: verum