let G be complete _Graph; :: thesis: 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); :: thesis: for H being inducedSubgraph of G,S holds H is complete

let H be inducedSubgraph of G,S; :: thesis: H is complete

for H being inducedSubgraph of G,S holds H is complete

let S be Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,S holds H is complete

let H be inducedSubgraph of G,S; :: thesis: H is complete

per cases
( S = {} or S <> {} )
;

end;

suppose
S <> {}
; :: thesis: H is complete

then A1:
the_Vertices_of H = S
by GLIB_000:def 37;

end;now :: thesis: for u, v being Vertex of H st u <> v holds

u,v are_adjacent

hence
H is complete
; :: thesis: verumu,v are_adjacent

let u, v be Vertex of H; :: thesis: ( u <> v implies u,v are_adjacent )

assume A2: u <> v ; :: thesis: 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 ; :: thesis: verum

end;assume A2: u <> v ; :: thesis: 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 ; :: thesis: verum