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_1:79, AMI_3:4; :: thesis: verum