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
A1: x in Vertices G and
A2: y in Vertices G and
A3: {x,y} in G ; :: thesis: {{},{x},{y},{x,y}} is Clique of G
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: ( not a in CompleteSGraph {x,y} or a in G )
assume A5: a in CompleteSGraph {x,y} ; :: thesis: a in G

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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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