:: deftheorem defines ProjectiveLines INCPROJ:def 1 :
for CPS being proper CollSp holds ProjectiveLines CPS = { B where B is Subset of CPS : B is LINE of CPS } ;