let G be SimpleGraph; :: thesis: for x being set st x in Vertices G holds
CompleteSGraph {x} c= G
let x be set ; :: thesis: ( x in Vertices G implies CompleteSGraph {x} c= G )
assume A: x in Vertices G ; :: thesis: CompleteSGraph {x} c= G
B: CompleteSGraph {x} = {{},{x}} by P1;
C: {} in G by SG1;
D: {x} in G by A, Vertices0;
thus CompleteSGraph {x} c= G by B, C, D, ZFMISC_1:32; :: thesis: verum