take { the loopfull _Graph} ; :: thesis: ( not { the loopfull _Graph} is empty & { the loopfull _Graph} is loopfull )
thus ( not { the loopfull _Graph} is empty & { the loopfull _Graph} is loopfull ) ; :: thesis: verum