let i be Element of SCM-Memory ; :: thesis: ( SCM-OK . i = SCM-Instr iff i in NAT )
thus ( SCM-OK . i = SCM-Instr implies i in NAT ) :: thesis: ( i in NAT implies SCM-OK . i = SCM-Instr )

proof

assume A1: SCM-OK . i = SCM-Instr ; :: thesis: i in NAT
assume not i in NAT ; :: thesis: contradiction
then ( i = NAT or i in SCM-Data-Loc ) by Lm1;
hence contradiction by A1, Def5, Th6; :: thesis: verum

end;

thus ( i in NAT implies SCM-OK . i = SCM-Instr ) by Def5; :: thesis: verum