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
A: x in X and
Aa: y in X ; :: thesis: {x,y} in CompleteSGraph X
B: {x,y} c= X by A, Aa, ZFMISC_1:32;
C: card {x,y} <= 2 by CARD_2:50;
thus {x,y} in CompleteSGraph X by C, B; :: thesis: verum