A1: ( 1 in Segm 8 & 2 in Segm 8 ) by GR_CY_1:10;
consider e1, e2 being Element of SCM-Data-Loc ;
A2: SCM-Instr S = (({[0 ,{} ]} \/ { [I,<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i1*>] where i1 is Element of NAT : verum } ) \/ ({ [7,<*i2,d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum } \/ { [5,<*d4,r*>] where d4 is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_1:4
.= ({[0 ,{} ]} \/ { [I,<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ ({ [6,<*i1*>] where i1 is Element of NAT : verum } \/ ({ [7,<*i2,d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum } \/ { [5,<*d4,r*>] where d4 is Element of SCM-Data-Loc , r is Element of S : verum } )) by XBOOLE_1:4
.= { [I,<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } \/ ({[0 ,{} ]} \/ ({ [6,<*i1*>] where i1 is Element of NAT : verum } \/ ({ [7,<*i2,d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum } \/ { [5,<*d4,r*>] where d4 is Element of SCM-Data-Loc , r is Element of S : verum } ))) by XBOOLE_1:4 ;
( 1 in {1,2,3,4} & 2 in {1,2,3,4} ) by ENUMSET1:def 2;
then ( [1,<*e1,e2*>] in { [I,<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } & [2,<*e1,e2*>] in { [I,<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } ) by A1;
then A3: ( [1,<*e1,e2*>] in SCM-Instr S & [2,<*e1,e2*>] in SCM-Instr S ) by A2, XBOOLE_0:def 3;
[1,<*e1,e2*>] <> [2,<*e1,e2*>] by ZFMISC_1:33;
hence not SCM-Instr S is trivial by A3, YELLOW_8:def 1; :: thesis: verum