let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated Mem-Struct of N
for d being data-only PartState of S holds not IC in dom d
let S be non empty IC-Ins-separated Mem-Struct of N; :: thesis: for d being data-only PartState of S holds not IC in dom d
let d be data-only PartState of S; :: thesis: not IC in dom d
dom d c= Data-Locations by Th31;
hence not IC in dom d by STRUCT_0:3; :: thesis: verum