let G be SimpleGraph; :: thesis: for S being Clique of G
for L being set st L c= Vertices S holds
G SubgraphInducedBy L is Clique of G
let S be Clique of G; :: thesis: for L being set st L c= Vertices S holds
G SubgraphInducedBy L is Clique of G
let L be set ; :: thesis: ( L c= Vertices S implies G SubgraphInducedBy L is Clique of G )
assume A1: L c= Vertices S ; :: thesis: G SubgraphInducedBy L is Clique of G
set g = G SubgraphInducedBy L;

now :: thesis: for x, y being set st x in union (G SubgraphInducedBy L) & y in union (G SubgraphInducedBy L) holds
{x,y} in G SubgraphInducedBy L

let x, y be set ; :: thesis: ( x in union (G SubgraphInducedBy L) & y in union (G SubgraphInducedBy L) implies {x,y} in G SubgraphInducedBy L )
assume that
A2: x in union (G SubgraphInducedBy L) and
A3: y in union (G SubgraphInducedBy L) ; :: thesis: {x,y} in G SubgraphInducedBy L
A4: x in L by A2, Lm7;
A5: y in L by A3, Lm7;
A6: {x,y} in S by A4, A5, A1, Th53;
thus {x,y} in G SubgraphInducedBy L by A4, A5, A6, Lm10; :: thesis: verum

end;

then G SubgraphInducedBy L = CompleteSGraph (Vertices (G SubgraphInducedBy L)) by Th32;
hence G SubgraphInducedBy L is Clique of G ; :: thesis: verum