theorem :: GLIB_015:54

for S1, S2 being Graph-membered set st S1 \/ S2 is edge-disjoint holds
( S1 is edge-disjoint & S2 is edge-disjoint )