let d1 be Element of SCM-Data-Loc ; :: thesis: [1,{} ,<*d1*>] in SCMPDS-Instr
[1,{} ,<*d1*>] in { [1,{} ,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ;
then [1,{} ,<*d1*>] in { [0 ,{} ,<*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 [1,{} ,<*d1*>] in ({ [0 ,{} ,<*k1*>] where k1 is Element of INT : verum } \/ { [1,{} ,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{} ,<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } by XBOOLE_0:def 3;
then [1,{} ,<*d1*>] in (({ [0 ,{} ,<*k1*>] where k1 is Element of INT : verum } \/ { [1,{} ,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{} ,<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ) \/ { [I2,{} ,<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } by XBOOLE_0:def 3;
hence [1,{} ,<*d1*>] in SCMPDS-Instr by XBOOLE_0:def 3; :: thesis: verum