theorem :: GLIB_006:69

for G2 being _Graph
for G1 being Supergraph of G2 holds
( the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G2) & the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) )