assume NAT in SCM-Data-Loc ; :: thesis: contradiction
then ex x, y being set st NAT = [x,y] by RELAT_1:def 1;
hence contradiction ; :: thesis: verum