let p be autonomic non programmed FinPartState of SCM ; :: thesis: IC SCM in dom p
A1: not dom p c= NAT by AMI_1:def 40;
dom p = (dom p) /\ the carrier of SCM by AMI_1:80, XBOOLE_1:28
.= ((dom p) /\ ({(IC SCM )} \/ SCM-Data-Loc )) \/ ((dom p) /\ NAT ) by AMI_3:4, XBOOLE_1:23 ;
then (dom p) /\ ({(IC SCM )} \/ SCM-Data-Loc ) <> {} by A1, XBOOLE_1:17;
then A2: ((dom p) /\ {(IC SCM )}) \/ ((dom p) /\ SCM-Data-Loc ) <> {} by XBOOLE_1:23;

per cases ( (dom p) /\ {(IC SCM )} <> {} or (dom p) /\ SCM-Data-Loc <> {} ) by A2;

suppose (dom p) /\ {(IC SCM )} <> {} ; :: thesis: IC SCM in dom p

then dom p meets {(IC SCM )} by XBOOLE_0:def 7;
hence IC SCM in dom p by ZFMISC_1:56; :: thesis: verum

end;

suppose A3: (dom p) /\ SCM-Data-Loc <> {} ; :: thesis: IC SCM in dom p

DataPart p <> {} by A3, AMI_3:72, RELAT_1:60, RELAT_1:90;
hence IC SCM in dom p by Th83; :: thesis: verum

end;

end;