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