theorem :: GLIB_015:51

for G1, G2 being _Graph holds
( {G1,G2} is vertex-disjoint iff ( G1 = G2 or the_Vertices_of G1 misses the_Vertices_of G2 ) )