let o be Object of SCM; :: thesis: ( o = IC or o in NAT or o is Data-Location )
the carrier of SCM = ({(IC )} \/ (Data-Locations SCM)) \/ NAT by COMPOS_1:160;
then ( o in {(IC )} \/ (Data-Locations SCM) or o in NAT ) by XBOOLE_0:def 3;
then ( o in {(IC )} or o in Data-Locations SCM or o in NAT ) by XBOOLE_0:def 3;
hence ( o = IC or o in NAT or o is Data-Location ) by AMI_3:72, AMI_3:def 2, TARSKI:def 1; :: thesis: verum