let N be with_non-empty_elements set ; :: thesis: for S being Mem-Struct of N
for p being PartState of S holds
( p is data-only iff dom p c= Data-Locations )
let S be Mem-Struct of N; :: thesis: for p being PartState of S holds
( p is data-only iff dom p c= Data-Locations )
let p be PartState of S; :: thesis: ( p is data-only iff dom p c= Data-Locations )
thus ( p is data-only implies dom p c= Data-Locations ) :: thesis: ( dom p c= Data-Locations implies p is data-only )

proof

A1: dom p c= the carrier of S by RELAT_1:def 18;
assume dom p misses {(IC )} ; :: according to MEMSTR_0:def 6 :: thesis: dom p c= Data-Locations
hence dom p c= Data-Locations by A1, XBOOLE_1:86; :: thesis: verum

end;

assume dom p c= Data-Locations ; :: thesis: p is data-only
hence dom p misses {(IC )} by XBOOLE_1:106; :: according to MEMSTR_0:def 6 :: thesis: verum