theorem :: GLIB_015:50

for S being Graph-membered set holds
( ( S is vertex-disjoint & S is edge-disjoint ) iff for G1, G2 being _Graph st G1 in S & G2 in S & G1 <> G2 holds
( the_Vertices_of G1 misses the_Vertices_of G2 & the_Edges_of G1 misses the_Edges_of G2 ) ) ;