let R1, R2 be Relation of D; :: thesis: ( ( for A, B being set holds
( [A,B] in R1 iff ( A in D & B in D & ( for a being set st a in A holds
ex b being set st
( b in B & [a,b] in the InternalRel of P ) ) ) ) ) & ( for A, B being set holds
( [A,B] in R2 iff ( A in D & B in D & ( for a being set st a in A holds
ex b being set st
( b in B & [a,b] in the InternalRel of P ) ) ) ) ) implies R1 = R2 )
assume that
A2: for A, B being set holds
( [A,B] in R1 iff ( A in D & B in D & ( for a being set st a in A holds
ex b being set st
( b in B & [a,b] in the InternalRel of P ) ) ) ) and
A3: for A, B being set holds
( [A,B] in R2 iff ( A in D & B in D & ( for a being set st a in A holds
ex b being set st
( b in B & [a,b] in the InternalRel of P ) ) ) ) ; :: thesis: R1 = R2
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [^,^] in R1 or [^,^] in R2 ) & ( not [^,^] in R2 or [^,^] in R1 ) )
reconsider a = x, b = y as set by TARSKI:1;
A4: ( [a,b] in R1 iff S₁[a,b] ) by A2;
( [a,b] in R2 iff S₁[a,b] ) by A3;
hence ( [x,y] in R1 iff [x,y] in R2 ) by A4; :: thesis: verum