let c be Element of SCM+FSA-Data-Loc ; :: thesis: [13,{},<*c*>] in SCM+FSA-Instr
reconsider x = 13 as Element of Segm 14 by NAT_1:45;
[x,{},<*c*>] in { [13,{},<*b1*>] where b1 is Element of SCM+FSA-Data-Loc : verum } ;
hence [13,{},<*c*>] in SCM+FSA-Instr by XBOOLE_0:def 3; :: thesis: verum