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