take NAT --> 0 ; :: thesis: not NAT --> 0 is finite
thus not NAT --> 0 is finite ; :: thesis: verum