let S be GraphUnionSet; :: thesis: for G being GraphUnion of S
for H being Element of S holds H is Subgraph of G
let G be GraphUnion of S; :: thesis: for H being Element of S holds H is Subgraph of G
let H be Element of S; :: thesis: H is Subgraph of G
the_Vertices_of H in the_Vertices_of S ;
then the_Vertices_of H c= union (the_Vertices_of S) by ZFMISC_1:74;
then A1: the_Vertices_of H c= the_Vertices_of G by Def25;
the_Source_of H in the_Source_of S ;
then the_Source_of H c= union (the_Source_of S) by ZFMISC_1:74;
then A2: the_Source_of H c= the_Source_of G by Def25;
the_Target_of H in the_Target_of S ;
then the_Target_of H c= union (the_Target_of S) by ZFMISC_1:74;
then the_Target_of H c= the_Target_of G by Def25;
then G is Supergraph of H by A1, A2, GLIB_006:63;
hence H is Subgraph of G by GLIB_006:57; :: thesis: verum