let G2 be _Graph; :: thesis: for G1 being Supergraph of G2 holds
( the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1 )
let G1 be Supergraph of G2; :: thesis: ( the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1 )
A1: ( dom (the_Source_of G2) = the_Edges_of G2 & dom (the_Target_of G2) = the_Edges_of G2 & dom (the_Source_of G1) = the_Edges_of G1 & dom (the_Target_of G1) = the_Edges_of G1 ) by GLIB_000:4;
A2: ( dom (the_Source_of G2) c= dom (the_Source_of G1) & dom (the_Target_of G2) c= dom (the_Target_of G1) ) by A1, Def9;
for e being object st e in dom (the_Source_of G2) holds
(the_Source_of G2) . e = (the_Source_of G1) . e by Def9;
hence the_Source_of G2 c= the_Source_of G1 by A2, GRFUNC_1:2; :: thesis: the_Target_of G2 c= the_Target_of G1
for e being object st e in dom (the_Target_of G2) holds
(the_Target_of G2) . e = (the_Target_of G1) . e by Def9;
hence the_Target_of G2 c= the_Target_of G1 by A2, GRFUNC_1:2; :: thesis: verum