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
not not InsCode i = 0 & ... & not InsCode i = 7 by Th7;
hence InsCode i <= 7 ; :: thesis: verum