let o be Object of SCM+FSA; :: thesis: ( not o in Data-Locations SCM+FSA or o is Int-Location or o is FinSeq-Location )
F: Data-Locations SCM+FSA = Int-Locations \/ FinSeq-Locations by SCMFSA_2:127;
assume o in Data-Locations SCM+FSA ; :: thesis: ( o is Int-Location or o is FinSeq-Location )
then ( o in Int-Locations or o in FinSeq-Locations ) by F, XBOOLE_0:def 3;
then ( o in SCM+FSA-Data-Loc or o in SCM+FSA-Data*-Loc ) ;
hence ( o is Int-Location or o is FinSeq-Location ) by SCMFSA_2:def 4, SCMFSA_2:def 5; :: thesis: verum