let p be non NAT -defined autonomic FinPartState of SCM+FSA ; :: thesis: IC SCM+FSA in dom p
A1: not dom p c= NAT by RELAT_1:def 18;
dom p = (dom p) /\ the carrier of SCM+FSA by AMI_1:80, XBOOLE_1:28
.= ((dom p) /\ ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) \/ ((dom p) /\ NAT ) by SCMFSA_2:8, XBOOLE_1:23 ;
then (dom p) /\ ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) <> {} by A1, XBOOLE_1:17;
then A2: ((dom p) /\ {(IC SCM+FSA )}) \/ ((dom p) /\ (Int-Locations \/ FinSeq-Locations )) <> {} by XBOOLE_1:23;

per cases ( (dom p) /\ {(IC SCM+FSA )} <> {} or (dom p) /\ (Int-Locations \/ FinSeq-Locations ) <> {} ) by A2;

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

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

end;

suppose (dom p) /\ (Int-Locations \/ FinSeq-Locations ) <> {} ; :: thesis: IC SCM+FSA in dom p

then DataPart p <> {} by RELAT_1:60, RELAT_1:90, SCMFSA_2:127;
hence IC SCM+FSA in dom p by Th14; :: thesis: verum

end;

end;