:: deftheorem Def19 defines edge-disjoint GLIB_015:def 19 :
for S being Graph-membered set holds
( S is edge-disjoint iff for G1, G2 being _Graph st G1 in S & G2 in S & G1 <> G2 holds
the_Edges_of G1 misses the_Edges_of G2 );