let R be Ring; :: thesis: for i being Element of SCM-Instr R holds InsCode i <= 7
let i be Element of SCM-Instr R; :: thesis: InsCode i <= 7
( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 ) by Th7;
hence InsCode i <= 7 ; :: thesis: verum