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 )
A1: 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 SCM+FSA-Data-Loc or o in SCM+FSA-Data*-Loc ) by A1, XBOOLE_0:def 3;
hence ( o is Int-Location or o is FinSeq-Location ) by SCMFSA_2:def 4, SCMFSA_2:def 5; :: thesis: verum