consider Z being Subset-Family of (NonZero V) such that
A2: ( Z = Class (Proportionality_as_EqRel_of V) & ProjectivePoints V = Z ) by Def7;
consider u being Element of V such that
A3: u <> 0. V by STRUCT_0:def 19;
A4: u in NonZero V by A3, ZFMISC_1:64;
set Y = Dir u;
Dir u in Z by A2, A4, EQREL_1:def 5;
hence not ProjectivePoints V is empty by A2; :: thesis: verum