:: deftheorem defines DataPart MEMSTR_0:def 8 :
for N being with_zero set
for S being Mem-Struct over N
for p being PartState of S holds DataPart p = p | (Data-Locations );