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