set a = the Int-Location ;
A1: the Int-Location in SCM+FSA-Data-Loc by SCMFSA_2:def 4;
assume not SCM+FSA-Data-Loc <> NAT ; :: thesis: contradiction
hence contradiction by A1, Th3; :: thesis: verum