let G be complete _Graph; for S being Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S holds H is complete
let S be Subset of (the_Vertices_of G); for H being inducedSubgraph of G,S holds H is complete
let H be inducedSubgraph of G,S; H is complete
per cases
( S = {} or S <> {} )
;
suppose
S <> {}
;
H is complete then A1:
the_Vertices_of H = S
by GLIB_000:def 37;
now for u, v being Vertex of H st u <> v holds
u,v are_adjacent let u,
v be
Vertex of
H;
( u <> v implies u,v are_adjacent )assume A2:
u <> v
;
u,v are_adjacent reconsider v2 =
v as
Vertex of
G by A1, TARSKI:def 3;
reconsider u2 =
u as
Vertex of
G by A1, TARSKI:def 3;
u2,
v2 are_adjacent
by A2, Def6;
then consider e being
object such that A3:
e Joins u2,
v2,
G
;
e Joins u,
v,
H
by A1, A3, Th19;
hence
u,
v are_adjacent
;
verum end; hence
H is
complete
;
verum end; end;