:: deftheorem Def18 defines vertex-disjoint GLIB_015:def 18 :
for S being Graph-membered set holds
( S is vertex-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 );