Data-Locations (STC N) = the carrier of (STC N) \ ({(IC )} \/ NAT)
.= the carrier of (STC N) \ ({NAT} \/ NAT) by Def11
.= ({NAT} \/ NAT) \ ({NAT} \/ NAT) by Def11
.= {} by XBOOLE_1:37 ;
hence DataPart p is empty ; :: thesis: verum