defpred S₁[ set , set ] 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 set 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