let l be Element of SCMPDS-Instr ; :: thesis: InsCode l <= 14
not not InsCode l = 0 & ... & not InsCode l = 14 by Th8;
hence InsCode l <= 14 ; :: thesis: verum