let R be Ring; :: thesis: for I being Instruction of (SCM R) holds InsCode I <= 7
let I be Instruction of (SCM R); :: thesis: InsCode I <= 7
set T = InsCode I;
( 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 Lm2;
hence InsCode I <= 7 ; :: thesis: verum