let S be non empty 1-sorted ; :: thesis: NAT <> SCM-Instr S

now

assume 2 in SCM-Instr S ; :: thesis: contradiction
then ( 2 in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or 2 in { [5,{},<*i,r*>] where i is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_0:def 3;
then ( 2 in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } or 2 in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or 2 in { [5,{},<*i,r*>] where i is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_0:def 3;
then ( 2 in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or 2 in { [6,<*i*>,{}] where i is Element of NAT : verum } or 2 in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or 2 in { [5,{},<*i,r*>] where i is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_0:def 3;
then ( 2 in {[0,{},{}]} or 2 in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or 2 in { [6,<*i*>,{}] where i is Element of NAT : verum } or 2 in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or 2 in { [5,{},<*i,r*>] where i is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_0:def 3;
then ( 2 = [0,{},{}] or ex I being Element of Segm 8 ex d1, d2 being Element of SCM-Data-Loc st
( 2 = [I,{},<*d1,d2*>] & I in {1,2,3,4} ) or ex i1 being Element of NAT st 2 = [6,<*i1*>,{}] or ex i2 being Element of NAT ex d3 being Element of SCM-Data-Loc st 2 = [7,<*i2*>,<*d3*>] or ex d4 being Element of SCM-Data-Loc ex r being Element of S st 2 = [5,{},<*d4,r*>] ) by TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

hence NAT <> SCM-Instr S ; :: thesis: verum