:: deftheorem Def2 defines Proj_Inc INCPROJ:def 2 :
for CPS being proper CollSp
for b₂ being Relation of the carrier of CPS,(ProjectiveLines CPS) holds
( b₂ = Proj_Inc CPS iff for x, y being object holds
( [x,y] in b₂ iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) );