consider e1, e2 being Element of SCM-Data-Loc ;
A1: 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 ;
( 2 in Segm 8 & 2 in {1,2,3,4} ) by ENUMSET1:def 2, NAT_1:45;
then [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} } ;
then A2: [2,<*e1,e2*>] in SCM-Instr S by A1, XBOOLE_0:def 3;
A3: [1,<*e1,e2*>] <> [2,<*e1,e2*>] by ZFMISC_1:33;
( 1 in Segm 8 & 1 in {1,2,3,4} ) by ENUMSET1:def 2, NAT_1:45;
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} } ;
then [1,<*e1,e2*>] in SCM-Instr S by A1, XBOOLE_0:def 3;
hence not SCM-Instr S is trivial by A2, A3, YELLOW_8:def 1; :: thesis: verum