assume SCM-Data-Loc meets NAT ; :: thesis: contradiction
then consider x being set such that
A1: x in SCM-Data-Loc and
A2: x in NAT by XBOOLE_0:3;
ex y, z being set st x = [y,z] by A1, RELAT_1:def 1;
hence contradiction by A2; :: thesis: verum