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

proof

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

end;

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