let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty AMI-Struct of IL,N
for p being PartState of S holds
( p is data-only iff dom p c= Data-Locations S )
let N be with_non-empty_elements set ; :: thesis: for S being non empty AMI-Struct of IL,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 IL,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

assume dom p misses {(IC S)} \/ IL ; :: according to AMI_1:def 50 :: thesis: dom p c= Data-Locations S
hence dom p c= Data-Locations S by Th80, XBOOLE_1:86; :: thesis: verum

end;

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