let G be SimpleGraph; :: thesis: for x, y being set st x in Vertices G & y in Vertices G & {x,y} in G holds
{{},{x},{y},{x,y}} is Clique of G
let x, y be set ; :: thesis: ( x in Vertices G & y in Vertices G & {x,y} in G implies {{},{x},{y},{x,y}} is Clique of G )
assume that
A: x in Vertices G and
B: y in Vertices G and
AB: {x,y} in G ; :: thesis: {{},{x},{y},{x,y}} is Clique of G
set C = CompleteSGraph {x,y};
D: CompleteSGraph {x,y} = {{},{x},{y},{x,y}} by P2;
CompleteSGraph {x,y} c= G

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in CompleteSGraph {x,y} or a in G )
assume A1: a in CompleteSGraph {x,y} ; :: thesis: a in G

per cases ( a = {} or a = {x} or a = {y} or a = {x,y} ) by A1, D, ENUMSET1:def 2;

suppose a = {} ; :: thesis: a in G

hence a in G by SG1; :: thesis: verum

end;

suppose a = {x} ; :: thesis: a in G

hence a in G by A, Vertices0; :: thesis: verum

end;

suppose a = {y} ; :: thesis: a in G

hence a in G by B, Vertices0; :: thesis: verum

end;

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

hence a in G by AB; :: thesis: verum

end;

end;

end;

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