let H be inducedSubgraph of G,V; :: thesis: H is Dcomplete

per cases ( V is non empty Subset of (the_Vertices_of G) or not V is non empty Subset of (the_Vertices_of G) ) ;

suppose V is non empty Subset of (the_Vertices_of G) ; :: thesis: H is Dcomplete

then A1: ( the_Vertices_of H = V & the_Edges_of H = G .edgesBetween V ) by GLIB_000:def 37;
let v, w be Vertex of H; :: according to GLIB_016:def 1 :: thesis: ( v <> w implies ex e being object st e DJoins v,w,H )
assume A2: v <> w ; :: thesis: ex e being object st e DJoins v,w,H
the_Vertices_of H c= the_Vertices_of G ;
then reconsider v9 = v, w9 = w as Vertex of G by TARSKI:def 3;
consider e being object such that
A3: e DJoins v9,w9,G by A2, Def1;
take e ; :: thesis: e DJoins v,w,H
( e Joins v9,w9,G & v9 in V & w9 in V ) by A1, A3, GLIB_000:16;
then ( e in the_Edges_of H & e is set ) by A1, GLIB_000:32, TARSKI:1;
hence e DJoins v,w,H by A3, GLIB_000:73; :: thesis: verum

end;

suppose V is not non empty Subset of (the_Vertices_of G) ; :: thesis: H is Dcomplete

then G == H by GLIB_000:def 37;
hence H is Dcomplete by Th4; :: thesis: verum

end;

end;