theorem :: INCPROJ:4

for CPS being proper CollSp
for x being set holds
( x is LINE of CPS iff x is LINE of (IncProjSp_of CPS) ) by Th1;