let E be set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of E st S is realistic holds
for l being Instruction-Location of S holds not IC S = l
let S be non empty IC-Ins-separated AMI-Struct of E; :: thesis: ( S is realistic implies for l being Instruction-Location of S holds not IC S = l )
assume Z: S is realistic ; :: thesis: for l being Instruction-Location of S holds not IC S = l
given l being Instruction-Location of S such that G: IC S = l ; :: thesis: contradiction
l in NAT by ORDINAL1:def 13;
hence contradiction by Def21, Z, G; :: thesis: verum