let G, H be set ; :: thesis: ( G c= H implies PairsOf G c= PairsOf H )
assume A: G c= H ; :: thesis: PairsOf G c= PairsOf H
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in PairsOf G or e in PairsOf H )
assume AA: e in PairsOf G ; :: thesis: e in PairsOf H
E: card e = 2 by AA, LEdges;
e in G by AA;
hence e in PairsOf H by A, E, LEdges; :: thesis: verum