let G1, G2, G3 be _Graph; :: thesis: ( G1 == G2 & G1 is Subgraph of G3 implies G2 is Subgraph of G3 )
assume that
A1: G1 == G2 and
A2: G1 is Subgraph of G3 ; :: thesis: G2 is Subgraph of G3
A3: the_Edges_of G1 = the_Edges_of G2 by A1;
A4: ( the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) by A1;
the_Vertices_of G1 = the_Vertices_of G2 by A1;
hence ( the_Vertices_of G2 c= the_Vertices_of G3 & the_Edges_of G2 c= the_Edges_of G3 ) by A2, A3, Def32; :: according to GLIB_000:def 32 :: thesis: for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . e = (the_Source_of G3) . e & (the_Target_of G2) . e = (the_Target_of G3) . e )
let e be set ; :: thesis: ( e in the_Edges_of G2 implies ( (the_Source_of G2) . e = (the_Source_of G3) . e & (the_Target_of G2) . e = (the_Target_of G3) . e ) )
assume e in the_Edges_of G2 ; :: thesis: ( (the_Source_of G2) . e = (the_Source_of G3) . e & (the_Target_of G2) . e = (the_Target_of G3) . e )
hence ( (the_Source_of G2) . e = (the_Source_of G3) . e & (the_Target_of G2) . e = (the_Target_of G3) . e ) by A2, A3, A4, Def32; :: thesis: verum