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

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

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

end;

end;