let I be Instruction of SCMPDS; :: thesis: ( I in {[0,{},{}]} implies InsCode I = 0 )
assume I in {[0,{},{}]} ; :: thesis: InsCode I = 0
then I = [0,{},{}] by TARSKI:def 1;
hence InsCode I = 0 ; :: thesis: verum