theorem :: NOMIN_3:4

for D being non empty set
for p, q being PartialPredicate of D holds PP_and (p,q) ||= p by Th3;