theorem :: PROJPL_1:25

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