let X be set ; :: thesis: for x, y being object st x <> y & {x,y} in X holds
{x,y} in PairsOf X
let x, y be object ; :: thesis: ( x <> y & {x,y} in X implies {x,y} in PairsOf X )
assume that
A1: x <> y and
A2: {x,y} in X ; :: thesis: {x,y} in PairsOf X
card {x,y} = 2 by A1, CARD_2:57;
hence {x,y} in PairsOf X by A2, Def1; :: thesis: verum