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
A4: for a, b being set holds
( [a,b] in R1 iff S₁[a,b] ) by A2;
A5: for a, b being set holds
( [a,b] in R2 iff S₁[a,b] ) by A3;
thus R1 = R2 from RELAT_1:sch 2(A4, A5); :: thesis: verum