consider p being PartState of S;
{} c= p by XBOOLE_1:2;
then reconsider p = {} as FinPartState of S ;
take p ; :: thesis: p is data-only
thus dom p misses {(IC S)} \/ NAT by RELAT_1:60, XBOOLE_1:65; :: according to COMPOS_1:def 23 :: thesis: verum