let p be PartState of S; :: thesis: ( p is empty implies p is data-only )
assume p is empty ; :: thesis: p is data-only
hence dom p misses {(IC )} by RELAT_1:38, XBOOLE_1:65; :: according to MEMSTR_0:def 6 :: thesis: verum