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

proof

assume A1: SCMPDS-OK . i = NAT ; :: thesis: i = NAT
assume A2: i <> NAT ; :: thesis: contradiction

per cases ( i in SCM-Data-Loc or i in NAT ) by A2, Lm1;

suppose i in SCM-Data-Loc ; :: thesis: contradiction

hence contradiction by A1, Def4, NUMBERS:27; :: thesis: verum

end;

suppose i in NAT ; :: thesis: contradiction

hence contradiction by A1, Def4, Th17; :: thesis: verum

end;

end;

end;

thus ( i = NAT implies SCMPDS-OK . i = NAT ) by Def4; :: thesis: verum