let M1, M2 be Subset of [: the carrier of R, the carrier of R:]; :: thesis: ( ( for x being set holds
( x in M1 iff ex a, b being Element of R st
( x = [a,b] & b in S ) ) ) & ( for x being set holds
( x in M2 iff ex a, b being Element of R st
( x = [a,b] & b in S ) ) ) implies M1 = M2 )
assume A2: for x being set holds
( x in M1 iff ex a, b being Element of R st
( x = [a,b] & b in S ) ) ; :: thesis: ( ex x being set st
( ( x in M2 implies ex a, b being Element of R st
( x = [a,b] & b in S ) ) implies ( ex a, b being Element of R st
( x = [a,b] & b in S ) & not x in M2 ) ) or M1 = M2 )
assume A3: for x being set holds
( x in M2 iff ex a, b being Element of R st
( x = [a,b] & b in S ) ) ; :: thesis: M1 = M2
A4: for x being object st x in M2 holds
x in M1

proof

let o be object ; :: thesis: ( o in M2 implies o in M1 )
assume o in M2 ; :: thesis: o in M1
then ex a, b being Element of R st
( o = [a,b] & b in S ) by A3;
hence o in M1 by A2; :: thesis: verum

end;

for o being object st o in M1 holds
o in M2

proof

let o be object ; :: thesis: ( o in M1 implies o in M2 )
assume o in M1 ; :: thesis: o in M2
then ex a, b being Element of R st
( o = [a,b] & b in S ) by A2;
hence o in M2 by A3; :: thesis: verum

end;

hence M1 = M2 by A4, TARSKI:2; :: thesis: verum