let G be SimpleGraph; 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; for L being set st L c= Vertices S holds
G SubgraphInducedBy L is Clique of G
let L be set ; ( L c= Vertices S implies G SubgraphInducedBy L is Clique of G )
assume A1:
L c= Vertices S
; G SubgraphInducedBy L is Clique of G
set g = G SubgraphInducedBy L;
now for x, y being set st x in union (G SubgraphInducedBy L) & y in union (G SubgraphInducedBy L) holds
{x,y} in G SubgraphInducedBy Llet x,
y be
set ;
( 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)
;
{x,y} in G SubgraphInducedBy LA4:
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;
verum end;
then
G SubgraphInducedBy L = CompleteSGraph (Vertices (G SubgraphInducedBy L))
by Th32;
hence
G SubgraphInducedBy L is Clique of G
; verum