take {} ; :: thesis: {} is non-empty
thus not {} in rng {} ; :: according to RELAT_1:def 9 :: thesis: verum