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

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

suppose S = {} ; :: thesis: H is complete

then H == G by GLIB_000:def 37;
hence H is complete by Th61; :: thesis: verum

end;

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

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

now :: thesis: for u, v being Vertex of H st u <> v holds
u,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;

hence H is complete ; :: thesis: verum

end;

end;