let G be _Graph; :: thesis: for G1, G2 being Subgraph of G st the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c= the_Edges_of G2 holds
G1 is Subgraph of G2
let G1, G2 be Subgraph of G; :: thesis: ( the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c= the_Edges_of G2 implies G1 is Subgraph of G2 )
assume that
A1: the_Vertices_of G1 c= the_Vertices_of G2 and
A2: the_Edges_of G1 c= the_Edges_of G2 ; :: thesis: G1 is Subgraph of G2
now :: thesis: for e being set st e in the_Edges_of G1 holds
( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e )
let e be set ; :: thesis: ( e in the_Edges_of G1 implies ( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e ) )
assume A3: e in the_Edges_of G1 ; :: thesis: ( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e )
hence (the_Source_of G1) . e = (the_Source_of G) . e by Def32
.= (the_Source_of G2) . e by A2, A3, Def32 ;
:: thesis: (the_Target_of G1) . e = (the_Target_of G2) . e
thus (the_Target_of G1) . e = (the_Target_of G) . e by A3, Def32
.= (the_Target_of G2) . e by A2, A3, Def32 ; :: thesis: verum
end;
hence G1 is Subgraph of G2 by A1, A2, Def32; :: thesis: verum