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 MCART_1:28;
( 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