let N be with_zero set ; :: thesis: for S being Mem-Struct over N
for p being PartState of S holds not IC in dom (DataPart p)
let S be Mem-Struct over 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 )} by RELAT_1:58;
then not IC in {(IC )} by A1, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum