set S1 = { [0 ,<*k1*>] where k1 is Element of INT : verum } ;
set S2 = { [1,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ;
set S3 = { [I2,<*d2,k2*>] where I2 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } ;
set S4 = { [I3,<*d3,k3,k4*>] where I3 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I3 in {4,5,6,7,8} } ;
set S5 = { [I4,<*d4,d5,k5,k6*>] where I4 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I4 in {9,10,11,12,13} } ;

now

assume 2 in SCMPDS-Instr ; :: thesis: contradiction
then ( 2 in (({ [0 ,<*k1*>] where k1 is Element of INT : verum } \/ { [1,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I2,<*d2,k2*>] where I2 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } ) \/ { [I3,<*d3,k3,k4*>] where I3 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I3 in {4,5,6,7,8} } or 2 in { [I4,<*d4,d5,k5,k6*>] where I4 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I4 in {9,10,11,12,13} } ) by XBOOLE_0:def 3;
then ( 2 in ({ [0 ,<*k1*>] where k1 is Element of INT : verum } \/ { [1,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I2,<*d2,k2*>] where I2 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } or 2 in { [I3,<*d3,k3,k4*>] where I3 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I3 in {4,5,6,7,8} } or 2 in { [I4,<*d4,d5,k5,k6*>] where I4 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I4 in {9,10,11,12,13} } ) by XBOOLE_0:def 3;
then ( 2 in { [0 ,<*k1*>] where k1 is Element of INT : verum } \/ { [1,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } or 2 in { [I2,<*d2,k2*>] where I2 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } or 2 in { [I3,<*d3,k3,k4*>] where I3 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I3 in {4,5,6,7,8} } or 2 in { [I4,<*d4,d5,k5,k6*>] where I4 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I4 in {9,10,11,12,13} } ) by XBOOLE_0:def 3;
then ( 2 in { [0 ,<*k1*>] where k1 is Element of INT : verum } or 2 in { [1,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } or 2 in { [I2,<*d2,k2*>] where I2 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } or 2 in { [I3,<*d3,k3,k4*>] where I3 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I3 in {4,5,6,7,8} } or 2 in { [I4,<*d4,d5,k5,k6*>] where I4 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I4 in {9,10,11,12,13} } ) by XBOOLE_0:def 3;
then ( ex k1 being Element of INT st 2 = [0 ,<*k1*>] or ex d1 being Element of SCM-Data-Loc st 2 = [1,<*d1*>] or ex I2 being Element of Segm 14 ex d2 being Element of SCM-Data-Loc ex k2 being Element of INT st
( 2 = [I2,<*d2,k2*>] & I2 in {2,3} ) or ex I3 being Element of Segm 14 ex d3 being Element of SCM-Data-Loc ex k1, k2 being Element of INT st
( 2 = [I3,<*d3,k1,k2*>] & I3 in {4,5,6,7,8} ) or ex I4 being Element of Segm 14 ex d4, d5 being Element of SCM-Data-Loc ex k5, k6 being Element of INT st
( 2 = [I4,<*d4,d5,k5,k6*>] & I4 in {9,10,11,12,13} ) ) ;
hence contradiction ; :: thesis: verum

end;

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