:: deftheorem Def8 defines * PROJPL_1:def 8 :
for G being IncProjSp
for a, b being POINT of G st a <> b holds
for b₄ being LINE of G holds
( b₄ = a * b iff {a,b} on b₄ );