theorem :: GLIB_000:73

for G1 being _Graph
for G2 being Subgraph of G1
for x, y, e being set st e in the_Edges_of G2 holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) ) by Def32;