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 A1: x in union G ; :: thesis: ex C being finite Clique of G st Vertices C = {x}
set C = CompleteSGraph {x};
A2: CompleteSGraph {x} = {{},{x}} by Th36;
reconsider C = CompleteSGraph {x} as finite Clique of G by A1, A2, Th50;
take C ; :: thesis: Vertices C = {x}
thus Vertices C = {x} by A2, Th8; :: thesis: verum