now :: thesis: not NAT in FinSeq-Locations

assume NAT in FinSeq-Locations ; :: thesis: contradiction
then A1: NAT in (NAT \/ [:{0},NAT:]) \ {[0,0]} by NUMBERS:def 4;
not NAT in NAT ;
then NAT in [:{0},NAT:] by A1, XBOOLE_0:def 3;
then ex x, y being object st NAT = [x,y] by RELAT_1:def 1;
hence contradiction ; :: thesis: verum

end;

then FinSeq-Locations misses {NAT} by ZFMISC_1:50;
then A2: FinSeq-Locations \ {NAT} = FinSeq-Locations by XBOOLE_1:83;
SCM-Data-Loc misses {NAT} by AMI_2:20, ZFMISC_1:50;
then A3: SCM-Data-Loc misses {NAT} ;
A4: SCM-Memory \ {NAT} = SCM-Data-Loc \ {NAT} by XBOOLE_1:40
.= Int-Locations by A3, XBOOLE_1:83 ;
thus Data-Locations = (SCM-Memory \/ FinSeq-Locations) \ {NAT} by SCMFSA_1:5, SUBSET_1:def 8
.= Int-Locations \/ FinSeq-Locations by A2, A4, XBOOLE_1:42 ; :: thesis: verum