let IL, N be set ; :: thesis: for S being non empty AMI-Struct of IL,N
for p being FinPartState of S holds not IC S in dom (DataPart p)
let S be non empty AMI-Struct of IL,N; :: thesis: for p being FinPartState of S holds not IC S in dom (DataPart p)
let p be FinPartState of S; :: thesis: not IC S in dom (DataPart p)
A1: dom (DataPart p) c= the carrier of S \ ({(IC S)} \/ IL) by RELAT_1:87;
assume IC S in dom (DataPart p) ; :: thesis: contradiction
then not IC S in {(IC S)} \/ IL 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