not INT c= NAT by NUMBERS:7, NUMBERS:17, XBOOLE_0:def 10;
hence not SCM+FSA-Data*-Loc is empty by XBOOLE_1:37; :: thesis: verum