consider Z being Subset-Family of (Proper_Vectors_of 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 Def8;
reconsider u = u as Element of V ;
A4: u in Proper_Vectors_of V by A3, Def4;
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