let i be Element of NAT ; :: thesis: ( not i in Data-Locations SCM+FSA & not IC in Data-Locations SCM+FSA )

A1: now

assume IC in FinSeq-Locations ; :: thesis: contradiction
then IC is FinSeq-Location by SCMFSA_2:12;
hence contradiction by SCMFSA_2:82; :: thesis: verum

end;

( not i in Int-Locations & not i in FinSeq-Locations ) by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_0:3;
hence not i in Data-Locations SCM+FSA by XBOOLE_0:def 3, SCMFSA_2:127; :: thesis: not IC in Data-Locations SCM+FSA

now

assume IC in Int-Locations ; :: thesis: contradiction
then IC is Int-Location by SCMFSA_2:11;
hence contradiction by SCMFSA_2:81; :: thesis: verum

end;

hence not IC in Data-Locations SCM+FSA by A1, XBOOLE_0:def 3, SCMFSA_2:127; :: thesis: verum