let G, H be set ; :: thesis: ( G c= H implies PairsOf G c= PairsOf H )
assume A1: G c= H ; :: thesis: PairsOf G c= PairsOf H
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in PairsOf G or e in PairsOf H )
reconsider ee = e as set by TARSKI:1;
assume A2: e in PairsOf G ; :: thesis: e in PairsOf H
A3: card ee = 2 by A2, Def1;
e in G by A2;
hence e in PairsOf H by A1, A3, Def1; :: thesis: verum