set X = ConFuncs P,Q;
let Y1, Y2 be Relation of (ConFuncs P,Q); :: thesis: ( ( for x, y being set holds
( [x,y] in Y1 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 ) ) ) ) & ( for x, y being set holds
( [x,y] in Y2 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 ) ) ) ) implies Y1 = Y2 )
defpred S₁[ set , set ] means ( $1 in ConFuncs P,Q & $2 in ConFuncs P,Q & ex f, g being Function of P,Q st
( $1 = f & $2 = g & f <= g ) );
( ( for x, y being set holds
( ( [x,y] in Y1 implies S₁[x,y] ) & ( S₁[x,y] implies [x,y] in Y1 ) & ( for x, y being set holds
( [x,y] in Y2 iff S₁[x,y] ) ) ) ) implies Y1 = Y2 )

proof

assume B1: for x, y being set holds
( ( [x,y] in Y1 implies S₁[x,y] ) & ( S₁[x,y] implies [x,y] in Y1 ) & ( for x, y being set holds
( [x,y] in Y2 iff S₁[x,y] ) ) ) ; :: thesis: Y1 = Y2
B2: for x1, y1 being Element of ConFuncs P,Q holds
( [x1,y1] in Y1 iff S₁[x1,y1] ) by B1;
B3: for x, y being Element of ConFuncs P,Q holds
( [x,y] in Y2 iff S₁[x,y] ) by B1;
thus Y1 = Y2 from RELSET_1:sch 4(B2, B3); :: thesis: verum

end;

hence ( ( for x, y being set holds
( [x,y] in Y1 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 ) ) ) ) & ( for x, y being set holds
( [x,y] in Y2 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 ) ) ) ) implies Y1 = Y2 ) ; :: thesis: verum