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