let G be SimpleGraph; :: thesis: for x being set st x in union G holds
ex C being finite Clique of G st Vertices C = {x}
let x be set ; :: thesis: ( x in union G implies ex C being finite Clique of G st Vertices C = {x} )
assume A: x in union G ; :: thesis: ex C being finite Clique of G st Vertices C = {x}
set C = CompleteSGraph {x};
B: CompleteSGraph {x} = {{},{x}} by P1;
reconsider C = CompleteSGraph {x} as finite Clique of G by A, B, SingleClique;
take C ; :: thesis: Vertices C = {x}
thus Vertices C = {x} by B, SingleVertices; :: thesis: verum