let da be Data-Location ; :: thesis: for p being PartState of SCM st da in dom p holds
da in dom (NPP p)
let p be PartState of SCM; :: thesis: ( da in dom p implies da in dom (NPP p) )
da in SCM-Data-Loc by AMI_3:def 2;
then A1: da in Data-Locations SCM by AMI_3:72;
assume da in dom p ; :: thesis: da in dom (NPP p)
then A2: da in dom (DataPart p) by A1, RELAT_1:86;
DataPart p c= NPP p by COMPOS_1:169;
then dom (DataPart p) c= dom (NPP p) by RELAT_1:25;
hence da in dom (NPP p) by A2; :: thesis: verum