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 A2: 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
then A3: for x1, y1 being Element of ConFuncs (P,Q) holds
( [x1,y1] in Y1 iff S₁[x1,y1] ) ;
A4: for x, y being Element of ConFuncs (P,Q) holds
( [x,y] in Y2 iff S₁[x,y] ) by A2;
thus Y1 = Y2 from RELSET_1:sch 4(A3, A4); :: 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