let l be Element of SCMPDS-Instr ; :: thesis: InsCode l <= 14
( InsCode l = 0 or InsCode l = 1 or InsCode l = 2 or InsCode l = 3 or InsCode l = 4 or InsCode l = 5 or InsCode l = 6 or InsCode l = 7 or InsCode l = 8 or InsCode l = 9 or InsCode l = 10 or InsCode l = 11 or InsCode l = 12 or InsCode l = 13 or InsCode l = 14 ) by Th8;
hence InsCode l <= 14 ; :: thesis: verum