A1: rng SCM-OK c= {INT} \/ {NAT} by RELAT_1:def 19;
assume {} in rng SCM-OK ; :: according to RELAT_1:def 9 :: thesis: contradiction
then ( {} in {INT} or {} in {NAT} ) by A1, XBOOLE_0:def 3;
then ( {} = INT or {} = NAT ) by TARSKI:def 1;
hence contradiction ; :: thesis: verum