let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for d being data-only PartState of S holds not IC in dom d
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over 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 Th6;
hence not IC in dom d by STRUCT_0:3; :: thesis: verum