let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated realistic AMI-Struct of N
for l, l1 being Instruction-Location of S holds not l in dom (Start-At l1)
let S be non empty IC-Ins-separated realistic AMI-Struct of N; :: thesis: for l, l1 being Instruction-Location of S holds not l in dom (Start-At l1)
let l, l1 be Instruction-Location of S; :: thesis: not l in dom (Start-At l1)
A: l in NAT by ORDINAL1:def 13;
assume l in dom (Start-At l1) ; :: thesis: contradiction
then NAT meets dom (Start-At l1) by XBOOLE_0:3, A;
hence contradiction by Th134; :: thesis: verum