take NAT --> the loopfull _Graph ; :: thesis: NAT --> the loopfull _Graph is loopfull
thus NAT --> the loopfull _Graph is loopfull ; :: thesis: verum