let p be PartState of S; :: thesis: ( p is data-only implies p is program-free )
assume dom p misses {(IC S)} \/ NAT ; :: according to COMPOS_1:def 23 :: thesis: p is program-free
then dom p misses NAT by XBOOLE_1:70;
hence p | NAT = {} by RELAT_1:95; :: according to COMPOS_1:def 29 :: thesis: verum