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

A1: now

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

end;

not a in {NAT} by A1;
hence a in the carrier of (SCM R) \ {NAT} by XBOOLE_0:def 5; :: thesis: verum