let X, x be set ; :: thesis: ( x in X implies {x} in CompleteSGraph X )
assume A: x in X ; :: thesis: {x} in CompleteSGraph X
B: {x} c= X by A, ZFMISC_1:31;
C: card {x} = 1 by CARD_1:30;
thus {x} in CompleteSGraph X by C, B; :: thesis: verum