let S be non empty 1-sorted ; :: thesis: [0,{},{}] in SCM-Instr S
[0,{},{}] in {[0,{},{}]} by TARSKI:def 1;
then [0,{},{}] 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} } by XBOOLE_0:def 3;
then [0,{},{}] 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 Nat : verum } by XBOOLE_0:def 3;
then [0,{},{}] 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 Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } by XBOOLE_0:def 3;
hence [0,{},{}] in SCM-Instr S by XBOOLE_0:def 3; :: thesis: verum