theorem :: GLIB_015:52

for G1, G2 being _Graph holds
( {G1,G2} is edge-disjoint iff ( G1 = G2 or the_Edges_of G1 misses the_Edges_of G2 ) )