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