:: deftheorem defines IncProjSp_of INCPROJ:def 3 :
for CPS being proper CollSp holds IncProjSp_of CPS = IncProjStr(# the carrier of CPS,(ProjectiveLines CPS),(Proj_Inc CPS) #);