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

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