consider e, f being Element of SCM-Data-Loc ;
( 1 in {1,2,3,4,5} & 1 is Element of Segm 9 ) by ENUMSET1:def 3, NAT_1:45;
then [1,<*e,f*>] in { [K,<*b,c*>] where K is Element of Segm 9, b, c is Element of SCM-Data-Loc : K in {1,2,3,4,5} } ;
then A1: [1,<*e,f*>] in SCM-Instr by XBOOLE_0:def 3;
( 2 in {1,2,3,4,5} & 2 is Element of Segm 9 ) by ENUMSET1:def 3, NAT_1:45;
then [2,<*e,f*>] in { [K,<*b,c*>] where K is Element of Segm 9, b, c is Element of SCM-Data-Loc : K in {1,2,3,4,5} } ;
then A2: [2,<*e,f*>] in SCM-Instr by XBOOLE_0:def 3;
[1,<*e,f*>] <> [2,<*e,f*>] by ZFMISC_1:33;
hence not SCM-Instr is trivial by A1, A2, YELLOW_8:def 1; :: thesis: verum