theorem :: INCPROJ:3

for CPS being proper CollSp
for x being set holds
( x is Point of CPS iff x is POINT of (IncProjSp_of CPS) ) ;