:: deftheorem Def15 defines PPFH PARTPR_2:def 13 :
for D being non empty set
for b₂ being Function of [:(Pr D),(FPrg D),(Pr D):],(Pr D) holds
( b₂ = PPFH D iff for p, q being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (b₂ . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (b₂ . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (b₂ . (p,f,q)) . d = FALSE ) ) ) ) );