theorem :: INCPROJ:2

for CPS being proper CollSp holds
( the Points of (IncProjSp_of CPS) = the carrier of CPS & the Lines of (IncProjSp_of CPS) = ProjectiveLines CPS & the Inc of (IncProjSp_of CPS) = Proj_Inc CPS ) ;