let o be Object of SCM+FSA ; :: thesis: ( o = IC SCM+FSA or o in NAT or o is Int-Location or o is FinSeq-Location )
( o in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} or o in NAT ) by SCMFSA_2:8, XBOOLE_0:def 3;
then ( o in Int-Locations \/ FinSeq-Locations or o in {(IC SCM+FSA )} or o in NAT ) by XBOOLE_0:def 3;
then ( o in Int-Locations or o in FinSeq-Locations or o in {(IC SCM+FSA )} or o in NAT ) by XBOOLE_0:def 3;
hence ( o = IC SCM+FSA or o in NAT or o is Int-Location or o is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12, TARSKI:def 1; :: thesis: verum