theorem Th71: :: GLIB_015:71

for F being non empty Graph-yielding Function holds
( F is edge-disjoint iff for x1, x2 being Element of dom F st x1 <> x2 holds
(the_Edges_of F) . x1 misses (the_Edges_of F) . x2 )