let x be set ; :: thesis: for b1, c1 being Element of SCM-Data-Loc st x in {1,2,3,4,5} holds
[x,<*b1,c1*>] in SCM-Instr
let b1, c1 be Element of SCM-Data-Loc ; :: thesis: ( x in {1,2,3,4,5} implies [x,<*b1,c1*>] in SCM-Instr )
assume A1: x in {1,2,3,4,5} ; :: thesis: [x,<*b1,c1*>] in SCM-Instr
then ( x = 1 or x = 2 or x = 3 or x = 4 or x = 5 ) by ENUMSET1:def 3;
then reconsider x = x as Element of Segm 9 by GR_CY_1:10;
[x,<*b1,c1*>] in { [J,<*b,c*>] where J is Element of Segm 9, b, c is Element of SCM-Data-Loc : J in {1,2,3,4,5} } by A1;
hence [x,<*b1,c1*>] in SCM-Instr by XBOOLE_0:def 3; :: thesis: verum