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