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

proof

X: dom p c= the carrier of S by RELAT_1:def 18;
assume dom p misses {(IC S)} \/ NAT ; :: according to AMI_1:def 51 :: thesis: dom p c= Data-Locations S
hence dom p c= Data-Locations S by X, XBOOLE_1:86; :: thesis: verum

end;

assume dom p c= Data-Locations S ; :: thesis: p is data-only
hence dom p misses {(IC S)} \/ NAT by XBOOLE_1:106; :: according to AMI_1:def 51 :: thesis: verum