let S be vertex-disjoint GraphUnionSet; :: thesis: for G being GraphUnion of S
for H being Element of S holds H is inducedSubgraph of G,(the_Vertices_of H)
let G be GraphUnion of S; :: thesis: for H being Element of S holds H is inducedSubgraph of G,(the_Vertices_of H)
let H be Element of S; :: thesis: H is inducedSubgraph of G,(the_Vertices_of H)
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;

now :: thesis: for x being object holds
( ( x in the_Edges_of H implies x in G .edgesBetween (the_Vertices_of H) ) & ( x in G .edgesBetween (the_Vertices_of H) implies x in the_Edges_of H ) )

let x be object ; :: thesis: ( ( x in the_Edges_of H implies x in G .edgesBetween (the_Vertices_of H) ) & ( x in G .edgesBetween (the_Vertices_of H) implies x in the_Edges_of H ) )

hereby :: thesis: ( x in G .edgesBetween (the_Vertices_of H) implies x in the_Edges_of H )

set v = (the_Source_of H) . x;
set w = (the_Target_of H) . x;
assume x in the_Edges_of H ; :: thesis: x in G .edgesBetween (the_Vertices_of H)
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: verum

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: x in the_Edges_of H
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: verum

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: verum