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

proof

assume A1: SCM-OK . i = INT ; :: thesis: i in SCM-Data-Loc
assume not i in SCM-Data-Loc ; :: thesis: contradiction
then i = NAT by Lm1;
hence contradiction by A1, Def5, NUMBERS:27; :: thesis: verum

end;

thus ( i in SCM-Data-Loc implies SCM-OK . i = INT ) by Def5; :: thesis: verum