let a be Element of NAT ; :: thesis: SCM-OK . a = SCM-Instr
a in NAT ;
then reconsider a = a as Element of SCM-Memory by Lm4;
SCM-OK . a = SCM-Instr by Th9;
hence SCM-OK . a = SCM-Instr ; :: thesis: verum