let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N holds NAT c= the carrier of S \ {(IC S)}
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N; :: thesis: NAT c= the carrier of S \ {(IC S)}
let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in NAT or i in the carrier of S \ {(IC S)} )
A1: NAT c= the carrier of S by AMI_1:def 3;
assume A2: i in NAT ; :: thesis: i in the carrier of S \ {(IC S)}
then i is Element of NAT ;
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