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: i in NAT by AMI_1:def 4;
then A2: not i in Int-Locations by SCMFSA_2:13, XBOOLE_0:3;
not i in FinSeq-Locations by A1, SCMFSA_2:14, XBOOLE_0:3;
hence not i in Int-Locations \/ FinSeq-Locations by A2, XBOOLE_0:def 3; :: thesis: not IC SCM+FSA in Int-Locations \/ FinSeq-Locations

A3: 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;

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;

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