for G being IncProjectivePlane
for a being POINT of G
for A, B being LINE of G st A <> B holds
( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) )