A2: rng SCM+FSA-OK c= {INT,(INT *)} \/ {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 {NAT} ) by A2, XBOOLE_0:def 3;
then ( {} = INT or {} = INT * or {} = NAT ) by TARSKI:def 1, TARSKI:def 2;
hence contradiction ; :: thesis: verum