take {} ; :: thesis: {} is non-zero
thus not 0 in rng {} ; :: according to ORDINAL1:def 15 :: thesis: verum