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; :: thesis: verum

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; :: thesis: verum