let it1, it2 be Subset of G; :: thesis: ( ( for e being set holds
( e in it1 iff ( e in G & card e = 2 ) ) ) & ( for e being set holds
( e in it2 iff ( e in G & card e = 2 ) ) ) implies it1 = it2 )
assume that
A: for e being set holds
( e in it1 iff ( e in G & card e = 2 ) ) and
B: for e being set holds
( e in it2 iff ( e in G & card e = 2 ) ) ; :: thesis: it1 = it2

now :: thesis: for x being set holds
( x in it1 iff x in it2 )

let x be set ; :: thesis: ( x in it1 iff x in it2 )
( x in it2 iff ( x in G & card x = 2 ) ) by B;
hence ( x in it1 iff x in it2 ) by A; :: thesis: verum

end;

hence it1 = it2 by TARSKI:1; :: thesis: verum