let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting IC-recognized AMI-Struct of N
for p being non NAT -defined autonomic FinPartState of holds IC in dom p
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting IC-recognized AMI-Struct of N; :: thesis: for p being non NAT -defined autonomic FinPartState of holds IC in dom p
let p be non NAT -defined autonomic FinPartState of ; :: thesis: IC in dom p
dom p c= the carrier of S by RELAT_1:def 18;
then A1: dom p = (dom p) /\ the carrier of S by XBOOLE_1:28
.= (dom p) /\ (({(IC )} \/ (Data-Locations S)) \/ NAT) by COMPOS_1:160
.= ((dom p) /\ ({(IC )} \/ (Data-Locations S))) \/ ((dom p) /\ NAT) by XBOOLE_1:23 ;
not dom p c= NAT by RELAT_1:def 18;
then (dom p) /\ ({(IC )} \/ (Data-Locations S)) <> {} by A1, XBOOLE_1:17;
then A2: ((dom p) /\ {(IC )}) \/ ((dom p) /\ (Data-Locations S)) <> {} by XBOOLE_1:23;

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

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

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

end;

suppose (dom p) /\ (Data-Locations S) <> {} ; :: thesis: IC in dom p

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

end;

end;