theorem :: NOMIN_3:8

for D being non empty set
for p being PartialPredicate of D holds PP_or (p,p) ||= p ;