theorem Th3: :: PROJRED1:3
for IPP being IncProjSp
for A, B being LINE of IPP st A <> B holds
ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A )