let S1, S2 be GraphUnionSet; :: thesis: for G1 being GraphUnion of S1
for G2 being GraphUnion of S2 st ( for H2 being Element of S2 ex H1 being Element of S1 st H2 is Subgraph of H1 ) holds
G2 is Subgraph of G1
let G1 be GraphUnion of S1; :: thesis: for G2 being GraphUnion of S2 st ( for H2 being Element of S2 ex H1 being Element of S1 st H2 is Subgraph of H1 ) holds
G2 is Subgraph of G1
let G2 be GraphUnion of S2; :: thesis: ( ( for H2 being Element of S2 ex H1 being Element of S1 st H2 is Subgraph of H1 ) implies G2 is Subgraph of G1 )
assume A1: for H2 being Element of S2 ex H1 being Element of S1 st H2 is Subgraph of H1 ; :: thesis: G2 is Subgraph of G1
now :: thesis: ( the_Vertices_of G2 c= the_Vertices_of G1 & the_Edges_of G2 c= the_Edges_of G1 & ( for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) ) )
now :: thesis: for x being object st x in the_Vertices_of G2 holds
x in the_Vertices_of G1
let x be object ; :: thesis: ( x in the_Vertices_of G2 implies x in the_Vertices_of G1 )
assume x in the_Vertices_of G2 ; :: thesis: x in the_Vertices_of G1
then x in union (the_Vertices_of S2) by GLIB_014:def 25;
then consider V being set such that
A2: ( x in V & V in the_Vertices_of S2 ) by TARSKI:def 4;
consider H2 being _Graph such that
A3: ( H2 in S2 & V = the_Vertices_of H2 ) by A2, GLIB_014:def 14;
consider H1 being Element of S1 such that
A4: H2 is Subgraph of H1 by A1, A3;
the_Vertices_of H2 c= the_Vertices_of H1 by A4, GLIB_000:def 32;
then A5: x in the_Vertices_of H1 by A2, A3;
the_Vertices_of H1 in the_Vertices_of S1 by GLIB_014:def 14;
then x in union (the_Vertices_of S1) by A5, TARSKI:def 4;
hence x in the_Vertices_of G1 by GLIB_014:def 25; :: thesis: verum
end;
hence the_Vertices_of G2 c= the_Vertices_of G1 by TARSKI:def 3; :: thesis: ( the_Edges_of G2 c= the_Edges_of G1 & ( for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) ) )
now :: thesis: for x being object st x in the_Edges_of G2 holds
x in the_Edges_of G1
let x be object ; :: thesis: ( x in the_Edges_of G2 implies x in the_Edges_of G1 )
assume x in the_Edges_of G2 ; :: thesis: x in the_Edges_of G1
then x in union (the_Edges_of S2) by GLIB_014:def 25;
then consider E being set such that
A6: ( x in E & E in the_Edges_of S2 ) by TARSKI:def 4;
consider H2 being _Graph such that
A7: ( H2 in S2 & E = the_Edges_of H2 ) by A6, GLIB_014:def 15;
consider H1 being Element of S1 such that
A8: H2 is Subgraph of H1 by A1, A7;
the_Edges_of H2 c= the_Edges_of H1 by A8, GLIB_000:def 32;
then A9: x in the_Edges_of H1 by A6, A7;
the_Edges_of H1 in the_Edges_of S1 by GLIB_014:def 15;
then x in union (the_Edges_of S1) by A9, TARSKI:def 4;
hence x in the_Edges_of G1 by GLIB_014:def 25; :: thesis: verum
end;
hence the_Edges_of G2 c= the_Edges_of G1 by TARSKI:def 3; :: thesis: for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e )
let e be set ; :: thesis: ( e in the_Edges_of G2 implies ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) )
set v = (the_Source_of G2) . e;
set w = (the_Target_of G2) . e;
assume e in the_Edges_of G2 ; :: thesis: ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e )
then consider H2 being Element of S2 such that
A10: e DJoins (the_Source_of G2) . e,(the_Target_of G2) . e,H2 by Th119, GLIB_000:def 14;
consider H1 being Element of S1 such that
A11: H2 is Subgraph of H1 by A1;
H1 is Subgraph of G1 by GLIB_014:21;
then H2 is Subgraph of G1 by A11, GLIB_000:43;
then e DJoins (the_Source_of G2) . e,(the_Target_of G2) . e,G1 by A10, GLIB_000:72;
hence ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) by GLIB_000:def 14; :: thesis: verum
end;
hence G2 is Subgraph of G1 by GLIB_000:def 32; :: thesis: verum