let s be State of SCM ; :: thesis: NAT c= dom s
NAT c= ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by XBOOLE_1:10;
hence NAT c= dom s by AMI_3:4, PARTFUN1:def 4; :: thesis: verum