take the loopless _Graph ; :: thesis: not the loopless _Graph is loopfull
thus not the loopless _Graph is loopfull ; :: thesis: verum