take {} ; :: thesis: {} is Z -valued
thus rng {} c= Z ; :: according to RELAT_1:def 19 :: thesis: verum