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