theorem Th7: :: INCPROJ:7
for CPS being proper CollSp
for a9 being Point of CPS ex b9 being Point of CPS st a9 <> b9