let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N holds IL c= the carrier of S \ {(IC S)}
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N holds IL c= the carrier of S \ {(IC S)}
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N; :: thesis: IL c= the carrier of S \ {(IC S)}
let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in IL or i in the carrier of S \ {(IC S)} )
A1: IL c= the carrier of S by AMI_1:def 3;
assume A2: i in IL ; :: thesis: i in the carrier of S \ {(IC S)}
then i is Instruction-Location of S by AMI_1:def 4;
then i <> IC S by AMI_1:48;
then not i in {(IC S)} by TARSKI:def 1;
hence i in the carrier of S \ {(IC S)} by A1, A2, XBOOLE_0:def 5; :: thesis: verum