[1,1] in SCM-Data-Loc by AMI_2:33;
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