NAT in {NAT } by TARSKI:def 1;
then NAT in {NAT } \/ SCM-Data-Loc by XBOOLE_0:def 3;
then NAT in SCM-Memory by XBOOLE_0:def 3;
hence NAT in SCM+FSA-Memory by XBOOLE_0:def 3; :: thesis: verum