let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty IC-Ins-separated realistic AMI-Struct of IL,N
for l, l1 being Instruction-Location of S holds not l in dom (Start-At l1)
let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated realistic AMI-Struct of IL,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 IL,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)
assume l in dom (Start-At l1) ; :: thesis: contradiction
then IL meets dom (Start-At l1) by XBOOLE_0:3;
hence contradiction by TW1; :: thesis: verum