let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for s being State of S holds Data-Locations S c= dom (NPP s)
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N; :: thesis: for s being State of S holds Data-Locations S c= dom (NPP s)
let s be State of S; :: thesis: Data-Locations S c= dom (NPP s)
A1: Data-Locations S = dom (DataPart s) by Th50;
DataPart s c= NPP s by Th169;
then dom (DataPart s) c= dom (NPP s) by RELAT_1:25;
hence Data-Locations S c= dom (NPP s) by A1; :: thesis: verum