hereby :: thesis: ( not InsCode i in {6,7,8} implies ex b₁ being Instruction of SCM+FSA st b₁ = i )

assume InsCode i in {6,7,8} ; :: thesis: ex ii being Instruction of SCM+FSA ex I being Instruction of SCM st
( I = i & ii = IncAddr I,k )
then ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by ENUMSET1:def 1;
then reconsider I = i as Instruction of SCM by SCMFSA_2:34;
reconsider ii = IncAddr I,k as Instruction of SCM+FSA by SCMFSA_2:38;
take ii = ii; :: thesis: ex I being Instruction of SCM st
( I = i & ii = IncAddr I,k )
take I = I; :: thesis: ( I = i & ii = IncAddr I,k )
thus ( I = i & ii = IncAddr I,k ) ; :: thesis: verum

end;

thus ( not InsCode i in {6,7,8} implies ex b₁ being Instruction of SCM+FSA st b₁ = i ) ; :: thesis: verum