:: deftheorem Def20 defines vertex-disjoint GLIB_015:def 20 :
for F being Graph-yielding Function holds
( F is vertex-disjoint iff for x1, x2 being object st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex G1, G2 being _Graph st
( G1 = F . x1 & G2 = F . x2 & the_Vertices_of G1 misses the_Vertices_of G2 ) );