let R be good Ring; :: thesis: for a being Data-Location of R holds not a in NAT
let a be Data-Location of R; :: thesis: not a in NAT
a in the carrier of (SCM R) \ (NAT \/ {NAT }) by SCMRING2:def 2;
then not a in NAT \/ {NAT } by XBOOLE_0:def 5;
hence not a in NAT by XBOOLE_0:def 3; :: thesis: verum