take X --> the _Graph ; :: thesis: ( not X --> the _Graph is empty & X --> the _Graph is Graph-yielding )
thus ( not X --> the _Graph is empty & X --> the _Graph is Graph-yielding ) ; :: thesis: verum