set e = the Element of SCM-Data-Loc ;
( 1 in {1,2,3,4,5} & 1 is Element of Segm 9 ) by ENUMSET1:def 3, NAT_1:44;
then [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] 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,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] 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:44;
then [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] 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,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr by XBOOLE_0:def 3;
[1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] <> [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] by XTUPLE_0:3;
hence not SCM-Instr is trivial by A1, A2, SUBSET_1:def 7; :: thesis: verum