let o be Object of SCM ; :: thesis: ( o = IC SCM or o in NAT or o is Data-Location )
( o in {(IC SCM )} \/ SCM-Data-Loc or o in NAT ) by AMI_5:23, XBOOLE_0:def 3;
then ( o in {(IC SCM )} or o in SCM-Data-Loc 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:def 2, TARSKI:def 1; :: thesis: verum