theorem :: PROJPL_1:32

for G being IncProjSp
for a, b, q, q1 being POINT of G st q on a * b & q on a * q1 & q <> a & q1 <> a & a <> b holds
q1 on a * b