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