set e1 = the 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 Nat : verum } ) \/ ( { [7,<*i2*>,<*d3*>] where i2 is 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 Nat : verum } \/ ( { [7,<*i2*>,<*d3*>] where i2 is 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 Nat : verum } \/ ( { [7,<*i2*>,<*d3*>] where i2 is 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:44;
then [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] 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,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr S by A1, XBOOLE_0:def 3;
A3: [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;
( 1 in Segm 8 & 1 in {1,2,3,4} ) by ENUMSET1:def 2, NAT_1:44;
then [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] 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,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr S by A1, XBOOLE_0:def 3;
hence not SCM-Instr S is trivial by A2, A3, SUBSET_1:def 7; :: thesis: verum