assume SCM+FSA-Data*-Loc meets SCM-Memory ; :: thesis: contradiction
then consider x being set such that
A1: x in SCM+FSA-Data*-Loc and
A2: x in SCM-Memory by XBOOLE_0:3;
A3: ( x in {NAT } \/ SCM-Data-Loc or x in NAT ) by A2, XBOOLE_0:def 3;
x in (NAT \/ [:{0 },NAT :]) \ {[0 ,0 ]} by A1, NUMBERS:def 4;
then A4: ( x in NAT or x in [:{0 },NAT :] ) by XBOOLE_0:def 3;

per cases ( x in {NAT } or x in SCM-Data-Loc or x in NAT ) by A3, XBOOLE_0:def 3;

suppose A5: x in {NAT } ; :: thesis: contradiction

then x = NAT by TARSKI:def 1;
then ex y, z being set st x = [y,z] by A4, RELAT_1:def 1;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum

end;

suppose x in SCM-Data-Loc ; :: thesis: contradiction

then consider k being Element of NAT such that
A6: x = [1,k] by AMI_2:32;
consider y, z being set such that
A7: y in {0 } and
z in NAT and
A8: x = [y,z] by A4, A6, ZFMISC_1:103;
y = 0 by A7, TARSKI:def 1;
hence contradiction by A6, A8, ZFMISC_1:33; :: thesis: verum

end;

suppose x in NAT ; :: thesis: contradiction

then consider k being Element of NAT such that
A9: x = k ;
thus contradiction by A1, A9, XBOOLE_0:def 5; :: thesis: verum

end;

end;