defpred S₁[ object , object ] means ex Y being set st
( $2 = Y & $1 in Y );
ex IT being Relation of the carrier of CPS,(ProjectiveLines CPS) st
for x, y being object holds
( [x,y] in IT iff ( x in the carrier of CPS & y in ProjectiveLines CPS & S₁[x,y] ) ) from RELSET_1:sch 1();
hence ex b₁ being Relation of the carrier of CPS,(ProjectiveLines CPS) st
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 ) ) ) ; :: thesis: verum