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