let S be vertex-disjoint GraphUnionSet; :: thesis:
let G be GraphUnion of S; :: thesis:
let H be Element of S; :: thesis:
A1: H is Subgraph of G by GLIB_014:21;
then A2: the_Vertices_of H is non empty Subset of (the_Vertices_of G) by GLIB_000:def 32;

let x be object ; :: thesis:

hereby :: thesis:

set v = (the_Source_of H) . x;
set w = (the_Target_of H) . x;
assume x in the_Edges_of H ; :: thesis:
then A3: x Joins (the_Source_of H) . x,(the_Target_of H) . x,H by GLIB_000:def 13;
then A4: ( (the_Source_of H) . x in the_Vertices_of H & (the_Target_of H) . x in the_Vertices_of H ) by GLIB_000:13;
x Joins (the_Source_of H) . x,(the_Target_of H) . x,G by A1, A3, GLIB_000:72;
hence x in G .edgesBetween (the_Vertices_of H) by A4, GLIB_000:32; :: thesis:

end;

set v = (the_Source_of G) . x;
set w = (the_Target_of G) . x;
assume x in G .edgesBetween (the_Vertices_of H) ; :: thesis:
then A5: ( (the_Source_of G) . x in the_Vertices_of H & x in the_Edges_of G ) by GLIB_000:31;
then x Joins (the_Source_of G) . x,(the_Target_of G) . x,G by GLIB_000:def 13;
then consider H9 being Element of S such that
A6: x Joins (the_Source_of G) . x,(the_Target_of G) . x,H9 by GLIBPRE1:117;
(the_Source_of G) . x in the_Vertices_of H9 by A6, GLIB_000:13;
then H = H9 by A5, Def18, XBOOLE_0:3;
hence x in the_Edges_of H by A6, GLIB_000:def 13; :: thesis:

end;

then the_Edges_of H = G .edgesBetween (the_Vertices_of H) by TARSKI:2;
hence H is inducedSubgraph of G,(the_Vertices_of H) by A1, A2, GLIB_000:def 37; :: thesis: