:: deftheorem Def9 defines * PROJPL_1:def 9 :
for G being IncProjectivePlane
for A, B being LINE of G st A <> B holds
for b₄ being POINT of G holds
( b₄ = A * B iff b₄ on A,B );