set X = ConFuncs (P,Q);
let Y1, Y2 be Relation of (ConFuncs (P,Q)); ( ( 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 S1[ 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 S1[x,y] ) & ( S1[x,y] implies [x,y] in Y1 ) & ( for x, y being set holds
( [x,y] in Y2 iff S1[x,y] ) ) ) ) implies Y1 = Y2 )
proof
assume A2:
for
x,
y being
set holds
( (
[x,y] in Y1 implies
S1[
x,
y] ) & (
S1[
x,
y] implies
[x,y] in Y1 ) & ( for
x,
y being
set holds
(
[x,y] in Y2 iff
S1[
x,
y] ) ) )
;
Y1 = Y2
then A3:
for
x1,
y1 being
Element of
ConFuncs (
P,
Q) holds
(
[x1,y1] in Y1 iff
S1[
x1,
y1] )
;
A4:
for
x,
y being
Element of
ConFuncs (
P,
Q) holds
(
[x,y] in Y2 iff
S1[
x,
y] )
by A2;
thus
Y1 = Y2
from RELSET_1:sch 4(A3, A4); 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 )
; verum