let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated realistic AMI-Struct of N
for l being Instruction-Location of S holds ProgramPart (Start-At l) = {}
let S be non empty IC-Ins-separated realistic AMI-Struct of N; :: thesis: for l being Instruction-Location of S holds ProgramPart (Start-At l) = {}
let l be Instruction-Location of S; :: thesis: ProgramPart (Start-At l) = {}
dom (Start-At l) misses NAT by Th134;
hence ProgramPart (Start-At l) = {} by RELAT_1:187; :: thesis: verum