theorem :: GLIB_015:77

for G1, G2 being _Graph holds
( <*G1,G2*> is edge-disjoint iff the_Edges_of G1 misses the_Edges_of G2 )