let a2 be Element of NAT ; :: thesis: [6,<*a2*>] in SCM-Instr
reconsider x = 6 as Element of Segm 9 by GR_CY_1:10;
[x,<*a2*>] in { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ;
then [x,<*a2*>] in {[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } by XBOOLE_0:def 3;
then [x,<*a2*>] in ({[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } by XBOOLE_0:def 3;
hence [6,<*a2*>] in SCM-Instr by XBOOLE_0:def 3; :: thesis: verum