set S1 = { [14,{},<*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 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } ;

[0,{},{}] in {[0,{},{}]} by TARSKI:def 1;

then [0,{},{}] in {[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } by XBOOLE_0:def 3;

then [0,{},{}] in ({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } by XBOOLE_0:def 3;

then [0,{},{}] in (({[0,{},{}]} \/ { [14,{},<*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 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } by XBOOLE_0:def 3;

then [0,{},{}] in ((({[0,{},{}]} \/ { [14,{},<*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 15, 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 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I3 in {4,5,6,7,8} } by XBOOLE_0:def 3;

hence [0,{},{}] in SCMPDS-Instr by XBOOLE_0:def 3; :: thesis: 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 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } ;

[0,{},{}] in {[0,{},{}]} by TARSKI:def 1;

then [0,{},{}] in {[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } by XBOOLE_0:def 3;

then [0,{},{}] in ({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } by XBOOLE_0:def 3;

then [0,{},{}] in (({[0,{},{}]} \/ { [14,{},<*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 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } by XBOOLE_0:def 3;

then [0,{},{}] in ((({[0,{},{}]} \/ { [14,{},<*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 15, 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 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I3 in {4,5,6,7,8} } by XBOOLE_0:def 3;

hence [0,{},{}] in SCMPDS-Instr by XBOOLE_0:def 3; :: thesis: verum