theorem Th7: :: INCPROJ:7

for CPS being proper CollSp
for a9 being Point of CPS ex b9 being Point of CPS st a9 <> b9