defpred S₁[ object , object ] means ex f, g being Function of P,Q st
( $1 = f & $2 = g & f <= g );
set X = ConFuncs (P,Q);
consider IT being Relation of (ConFuncs (P,Q)),(ConFuncs (P,Q)) such that
A1: for x, y being object holds
( [x,y] in IT iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & S₁[x,y] ) ) from RELSET_1:sch 1();
take IT ; :: thesis: for x, y being set holds
( [x,y] in IT iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) )
thus for x, y being set holds
( [x,y] in IT iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) by A1; :: thesis: verum