consider p being FinPartState 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 AMI_1:def 51 :: thesis: verum