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