let l be Element of SCM-Instr ; :: thesis: InsCode l <= 8
( 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 ) by Th9;
hence InsCode l <= 8 ; :: thesis: verum