let N be non empty with_non-empty_elements set ; :: thesis: for x being set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N st x in Data-Locations S holds
for p being PartState of S st x in dom p holds
x in dom (NPP p)
let x be set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N st x in Data-Locations S holds
for p being PartState of S st x in dom p holds
x in dom (NPP p)
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: ( x in Data-Locations S implies for p being PartState of S st x in dom p holds
x in dom (NPP p) )
assume Z1: x in Data-Locations S ; :: thesis: for p being PartState of S st x in dom p holds
x in dom (NPP p)
let p be PartState of S; :: thesis: ( x in dom p implies x in dom (NPP p) )
assume Z2: x in dom p ; :: thesis: x in dom (NPP p)
DataPart p c= NPP p by Lm169;
then B: dom (DataPart p) c= dom (NPP p) by RELAT_1:25;
x in (Data-Locations S) /\ (dom p) by Z1, Z2, XBOOLE_0:def 4;
then x in dom (DataPart p) by RELAT_1:90;
hence x in dom (NPP p) by B; :: thesis: verum