consider e, f being Element of SCM-Data-Loc ;
A1: ( 1 in {1,2,3,4,5} & 2 in {1,2,3,4,5} ) by ENUMSET1:def 3;
( 1 is Element of Segm 9 & 2 is Element of Segm 9 ) by GR_CY_1:10;
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} } & [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} } ) by A1;
then A2: ( [1,<*e,f*>] in SCM-Instr & [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 A2, YELLOW_8:def 1; :: thesis: verum