:: deftheorem Def21 defines edge-disjoint GLIB_015:def 21 :
for F being Graph-yielding Function holds
( F is edge-disjoint iff for x1, x2 being object st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex G1, G2 being _Graph st
( G1 = F . x1 & G2 = F . x2 & the_Edges_of G1 misses the_Edges_of G2 ) );