(p \ (ProgramPart p)) | NAT = (p \ (p | NAT )) | NAT
.= {} by RELAT_1:216 ;
hence (NPP p) | NAT = {} ; :: according to COMPOS_1:def 29 :: thesis: verum