theorem :: GLIB_015:72

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