[1,1] in Data-Locations SCM by AMI_2:33, AMI_3:72;
then reconsider a = [1,1] as Object of (SCM R) by Def1;
take a ; :: thesis: a in the carrier of (SCM R) \ (NAT \/ {NAT})

A1: now

assume a in {NAT} ; :: thesis: contradiction
then a = NAT by TARSKI:def 1;
hence contradiction by ARYTM_3:36; :: thesis: verum

end;

not [1,1] in NAT by ARYTM_3:38;
then not a in NAT \/ {NAT} by A1, XBOOLE_0:def 3;
hence a in the carrier of (SCM R) \ (NAT \/ {NAT}) by XBOOLE_0:def 5; :: thesis: verum