:: deftheorem Def22 defines vertex-disjoint GLIB_015:def 22 :
for F being non empty Graph-yielding Function holds
( F is vertex-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) );