let S be non empty 1-sorted ; for i1 being Nat holds [6,<*i1*>,{}] in SCM-Instr S
let i1 be Nat; [6,<*i1*>,{}] in SCM-Instr S
reconsider I1 = i1 as Element of NAT by ORDINAL1:def 12;
[6,<*I1*>,{}] in { [6,<*i*>,{}] where i is Nat : verum }
;
then
[6,<*I1*>,{}] 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
[6,<*I1*>,{}] 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
[6,<*i1*>,{}] in SCM-Instr S
by XBOOLE_0:def 3; verum