theorem Th9: :: PROJPL_1:9

for G being IncProjStr
for a being POINT of G
for A, B being LINE of G st G is IncProjSp & A <> B holds
ex b being POINT of G st
( b on A & b |' B & a <> b )