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

proof

let u be object ; :: thesis: ( u in M2 implies u in M1 )
assume u in M2 ; :: thesis: u in M1
then ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) by A3;
hence u in M1 by A2; :: thesis: verum

end;

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

proof

let u be object ; :: thesis: ( u in M1 implies u in M2 )
assume u in M1 ; :: thesis: u in M2
then ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) by A2;
hence u in M2 by A3; :: thesis: verum

end;

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