now

assume 2 in SCM-Instr ; :: thesis: contradiction
then ( 2 in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or 2 in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ) by XBOOLE_0:def 3;
then ( 2 in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } or 2 in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or 2 in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ) by XBOOLE_0:def 3;
then ( 2 in {[SCM-Halt,{},{}]} or 2 in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } or 2 in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or 2 in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ) by XBOOLE_0:def 3;
then ( 2 = [SCM-Halt,{},{}] or ex J being Element of Segm 9 ex a being Element of NAT st
( 2 = [J,<*a*>,{}] & J = 6 ) or ex K being Element of Segm 9 ex a1 being Element of NAT ex b1 being Element of SCM-Data-Loc st
( 2 = [K,<*a1*>,<*b1*>] & K in {7,8} ) or ex I being Element of Segm 9 ex b, c being Element of SCM-Data-Loc st
( 2 = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ) by TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

hence ( SCM-Instr <> INT & NAT <> SCM-Instr ) by INT_1:def 2; :: thesis: verum