take NAT --> the Cycle-like _Graph ; :: thesis: ( not NAT --> the Cycle-like _Graph is empty & NAT --> the Cycle-like _Graph is Cycle-like )
thus ( not NAT --> the Cycle-like _Graph is empty & NAT --> the Cycle-like _Graph is Cycle-like ) ; :: thesis: verum