for N being with_zero set
for S being Mem-Struct over N
for p being PartState of S holds
( p is data-only iff dom p c= Data-Locations ) by RELAT_1:def 18, XBOOLE_1:86, XBOOLE_1:106;