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