let R be Ring; :: thesis: for a being Data-Location of R holds a <> IC
let a be Data-Location of R; :: thesis: a <> IC
a in SCM-Data-Loc by AMI_2:def 16;
then a <> NAT by AMI_2:20;
hence a <> IC by SCMRING2:8; :: thesis: verum