let R be good Ring; :: thesis: for s being State of (SCM R) holds NAT c= dom s
let s be State of (SCM R); :: thesis: NAT c= dom s
A1: dom s = the carrier of (SCM R) by AMI_1:79;
NAT c= ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT by XBOOLE_1:7;
hence NAT c= dom s by A1, Th14; :: thesis: verum