let I be Instruction of SCMPDS; :: thesis: ( I in { [14,{},<*k1*>] where k1 is Element of INT : verum } implies InsCode I = 14 )
assume I in { [14,{},<*k1*>] where k1 is Element of INT : verum } ; :: thesis: InsCode I = 14
then ex k1 being Element of INT st I = [14,{},<*k1*>] ;
hence InsCode I = 14 ; :: thesis: verum