take I --> NAT ; :: thesis: ( I --> NAT is V5() & I --> NAT is countable )
thus ( I --> NAT is V5() & I --> NAT is countable ) ; :: thesis: verum