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

proof

assume p is data-only ; :: thesis: DataPart p = p
then dom p c= Data-Locations S by Th31;
hence DataPart p = p by RELAT_1:97; :: thesis: verum

end;

assume DataPart p = p ; :: thesis: p is data-only
then dom p c= Data-Locations S by RELAT_1:87;
hence p is data-only by Th31; :: thesis: verum