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,{},<*d1,k2*>] where I2 is Element of Segm 14, d1 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,{},<*d1,k2*>] where I2 is Element of Segm 14, d1 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} } ) \/ { [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} } ;
then ( 2 in (( { [0,{},<*k1*>] where k1 is Element of INT : verum } \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I2,{},<*d1,k2*>] where I2 is Element of Segm 14, d1 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,{},<*d1,k2*>] where I2 is Element of Segm 14, d1 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,{},<*d1,k2*>] where I2 is Element of Segm 14, d1 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,{},<*d1,k2*>] where I2 is Element of Segm 14, d1 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 d1 being Element of SCM-Data-Loc ex k2 being Element of INT st
( 2 = [I2,{},<*d1,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