let G be SimpleGraph; :: thesis: for x being set st x in Vertices G holds
{{},{x}} is Clique of G
let x be set ; :: thesis: ( x in Vertices G implies {{},{x}} is Clique of G )
assume A1: x in Vertices G ; :: thesis: {{},{x}} is Clique of G
set C = CompleteSGraph {x};
A2: CompleteSGraph {x} = {{},{x}} by Th36;
thus {{},{x}} is Clique of G by A2, A1, Th39; :: thesis: verum