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