let i be Instruction-Location of SCM+FSA ; :: thesis: ( not i in Int-Locations \/ FinSeq-Locations & not IC SCM+FSA in Int-Locations \/ FinSeq-Locations )

A1: now

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

end;

i in NAT by AMI_1:def 4;
then ( not i in Int-Locations & not i in FinSeq-Locations ) by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_0:3;
hence not i in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3; :: thesis: not IC SCM+FSA in Int-Locations \/ FinSeq-Locations

now

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

end;

hence not IC SCM+FSA in Int-Locations \/ FinSeq-Locations by A1, XBOOLE_0:def 3; :: thesis: verum