:: deftheorem Def5 defines ProjectivePoints ANPROJ_1:def 5 :
for V being RealLinearSpace
for b₂ being set holds
( b₂ = ProjectivePoints V iff ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b₂ = Y ) );