theorem Th2: :: MEMSTR_0:2

for N being with_zero set
for S being non empty with_non-empty_values Mem-Struct over N
for s being State of S holds IC in dom s