let S be non empty 1-sorted ; :: thesis: for i1 being Element of NAT holds [6,<*i1*>,{} ] in SCM-Instr S
let i1 be Element of NAT ; :: thesis: [6,<*i1*>,{} ] in SCM-Instr S
reconsider I1 = i1 as Element of NAT ;
[6,<*I1*>,{} ] in { [6,<*i*>,{} ] where i is Element of 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 Element of 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 Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of 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; :: thesis: verum