let R be good Ring; :: thesis: ( not R is trivial implies for p being non NAT -defined autonomic FinPartState of holds IC (SCM R) in dom p )
assume A1: not R is trivial ; :: thesis: for p being non NAT -defined autonomic FinPartState of holds IC (SCM R) in dom p
let p be non NAT -defined autonomic FinPartState of ; :: thesis: IC (SCM R) in dom p
A2: not dom p c= NAT by RELAT_1:def 18;
dom p c= the carrier of (SCM R) by RELAT_1:def 18;
then dom p = (dom p) /\ the carrier of (SCM R) by XBOOLE_1:28
.= (dom p) /\ (({(IC (SCM R))} \/ (Data-Locations SCM)) \/ NAT) by Th1
.= ((dom p) /\ ({(IC (SCM R))} \/ (Data-Locations SCM))) \/ ((dom p) /\ NAT) by XBOOLE_1:23 ;
then (dom p) /\ ({(IC (SCM R))} \/ (Data-Locations SCM)) <> {} by A2, XBOOLE_1:17;
then A3: ((dom p) /\ {(IC (SCM R))}) \/ ((dom p) /\ (Data-Locations SCM)) <> {} by XBOOLE_1:23;

per cases ( (dom p) /\ {(IC (SCM R))} <> {} or (dom p) /\ (Data-Locations SCM) <> {} ) by A3;

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

hence IC (SCM R) in dom p by Lm1; :: thesis: verum

end;

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

Data-Locations (SCM R) = Data-Locations SCM by SCMRING2:31;
then DataPart p <> {} by A4, RELAT_1:60, RELAT_1:90;
hence IC (SCM R) in dom p by A1, Th24; :: thesis: verum

end;

end;