let I be Instruction of SCMPDS ; :: thesis: ( not I in { [I1,<*d1,k1*>] where I1 is Element of Segm 14, d1 is Element of SCM-Data-Loc , k1 is Element of INT : I1 in {2,3} } or InsCode I = 2 or InsCode I = 3 )
assume I in { [I1,<*d1,k1*>] where I1 is Element of Segm 14, d1 is Element of SCM-Data-Loc , k1 is Element of INT : I1 in {2,3} } ; :: thesis: ( InsCode I = 2 or InsCode I = 3 )
then consider I1 being Element of Segm 14, d1 being Element of SCM-Data-Loc , k1 being Element of INT such that
A1: ( I = [I1,<*d1,k1*>] & I1 in {2,3} ) ;
( I1 = 2 or I1 = 3 ) by A1, TARSKI:def 2;
hence ( InsCode I = 2 or InsCode I = 3 ) by A1, MCART_1:7; :: thesis: verum