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