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 A1: x in Vertices G ; :: thesis: CompleteSGraph {x} c= G
A2: CompleteSGraph {x} = {{},{x}} by Th36;
A3: {} in G by Th20;
A4: {x} in G by A1, Th24;
thus CompleteSGraph {x} c= G by A2, A3, A4, ZFMISC_1:32; :: thesis: verum