theorem :: GLIB_015:53

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