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