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

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

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

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

end;

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

then DataPart p <> {} by RELAT_1:60, RELAT_1:90, SCMPDS_2:100;
hence IC SCMPDS in dom p by Th16; :: thesis: verum

end;

end;