let N be set ; :: thesis: for S being non empty stored-program COM-Struct of N holds the carrier of S = ({(IC )} \/ (Data-Locations S)) \/ NAT
let S be non empty stored-program COM-Struct of N; :: thesis: the carrier of S = ({(IC )} \/ (Data-Locations S)) \/ NAT
NAT c= the carrier of S by Def2;
then {(IC )} \/ NAT c= the carrier of S by XBOOLE_1:8;
hence the carrier of S = (Data-Locations S) \/ ({(IC )} \/ NAT) by XBOOLE_1:45
.= ({(IC )} \/ (Data-Locations S)) \/ NAT by XBOOLE_1:4 ;
:: thesis: verum