let G be SimpleGraph; :: thesis:
let x, y be set ; :: thesis:
assume that
A1: x in Vertices G and
A2: y in Vertices G and
A3: {x,y} in G ; :: thesis:
set C = CompleteSGraph {x,y};
A4: CompleteSGraph {x,y} = {{},{x},{y},{x,y}} by Th37;
CompleteSGraph {x,y} c= G

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A5: a in CompleteSGraph {x,y} ; :: thesis:

per cases by A5, A4, ENUMSET1:def 2;

suppose a = {} ; :: thesis:

hence a in G by Th20; :: thesis:

end;

suppose a = {x} ; :: thesis:

hence a in G by A1, Th24; :: thesis:

end;

suppose a = {y} ; :: thesis:

hence a in G by A2, Th24; :: thesis:

end;

suppose a = {x,y} ; :: thesis:

hence a in G by A3; :: thesis:

end;

end;

end;

hence {{},{x},{y},{x,y}} is Clique of G by Th37; :: thesis: