let X be set ; :: thesis: for x, y being set st x in X & y in X holds
{x,y} in CompleteSGraph X
let x, y be set ; :: thesis: ( x in X & y in X implies {x,y} in CompleteSGraph X )
assume that
A1: x in X and
A2: y in X ; :: thesis: {x,y} in CompleteSGraph X
A3: {x,y} c= X by A1, A2, ZFMISC_1:32;
A4: card {x,y} <= 2 by CARD_2:50;
thus {x,y} in CompleteSGraph X by A4, A3; :: thesis: verum