let a be Int_position ; :: thesis: for p being PartState of SCMPDS st a in dom p holds
a in dom (NPP p)
let p be PartState of SCMPDS; :: thesis: ( a in dom p implies a in dom (NPP p) )
a in SCM-Data-Loc by SCMPDS_2:def 2;
then A1: a in Data-Locations SCMPDS by SCMPDS_2:100;
assume a in dom p ; :: thesis: a in dom (NPP p)
then A2: a 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 a in dom (NPP p) by A2; :: thesis: verum