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