theorem Th1: :: INCPROJ:1

for CPS being proper CollSp
for x being set holds
( x is LINE of CPS iff x is Element of ProjectiveLines CPS )