theorem Th3: :: MEMSTR_0:3

for N being with_zero set
for S being Mem-Struct over N
for p being PartState of S holds not IC in dom (DataPart p)