( the carrier of S \ ({(IC S)} \/ NAT) c= the carrier of S \ NAT & dom (DataPart p) c= the carrier of S \ ({(IC S)} \/ NAT) ) by RELAT_1:87, XBOOLE_1:7, XBOOLE_1:34;
then dom (DataPart p) c= the carrier of S \ NAT by XBOOLE_1:1;
then A1: dom (DataPart p) misses NAT by XBOOLE_1:64, XBOOLE_1:79;
dom (DataPart p) misses {(IC S)} by Th11, ZFMISC_1:56;
hence dom (DataPart p) misses {(IC S)} \/ NAT by A1, XBOOLE_1:70; :: according to COMPOS_1:def 23 :: thesis: verum