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