consider u being Element of V such that
A1:
u <> 0. V
by STRUCT_0:def 18;
set Y = Dir u;
consider Z being Subset-Family of (NonZero V) such that
A2:
Z = Class (Proportionality_as_EqRel_of V)
and
A3:
ProjectivePoints V = Z
by Def5;
u in NonZero V
by A1, ZFMISC_1:56;
then
Dir u in Z
by A2, EQREL_1:def 3;
hence
not ProjectivePoints V is empty
by A3; verum