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
( dom s = the carrier of (SCM R) & NAT c= ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT ) by PARTFUN1:def 4, XBOOLE_1:7;
hence NAT c= dom s by Th1; :: thesis: verum