take <* the _Graph*> ; :: thesis: ( not <* the _Graph*> is empty & <* the _Graph*> is vertex-disjoint & <* the _Graph*> is edge-disjoint )
thus ( not <* the _Graph*> is empty & <* the _Graph*> is vertex-disjoint & <* the _Graph*> is edge-disjoint ) ; :: thesis: verum