let X, x, y be set ; :: thesis: ( x <> y & {x,y} in X implies {x,y} in PairsOf X )
assume that
A: x <> y and
B: {x,y} in X ; :: thesis: {x,y} in PairsOf X
card {x,y} = 2 by A, CARD_2:57;
hence {x,y} in PairsOf X by B, LEdges; :: thesis: verum