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

per cases ( (dom p) /\ {(IC SCM)} <> {} or (dom p) /\ (Data-Locations SCM) <> {} ) 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 (dom p) /\ (Data-Locations SCM) <> {} ; :: thesis: IC SCM in dom p

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

end;

end;