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