let N be set ; :: thesis: for S being non empty COM-Struct of N
for p being PartState of S holds not IC in dom (DataPart p)
let S be non empty COM-Struct of N; :: thesis: for p being PartState of S holds not IC in dom (DataPart p)
let p be PartState of S; :: thesis: not IC in dom (DataPart p)
assume A1: IC in dom (DataPart p) ; :: thesis: contradiction
dom (DataPart p) c= the carrier of S \ ({(IC )} \/ NAT) by RELAT_1:87;
then not IC in {(IC )} \/ NAT by A1, XBOOLE_0:def 5;
then not IC in {(IC )} by XBOOLE_0:def 3;
hence contradiction by TARSKI:def 1; :: thesis: verum