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