for x being object
for D being non empty set
for p, q being PartialPredicate of D
for f being BinominativeFunction of D holds
( not x in dom (PP_FH (p,f,q)) or ( x in dom p & p . x = FALSE ) or ( x in dom (q * f) & (q * f) . x = TRUE ) or ( x in dom p & p . x = TRUE & x in dom (q * f) & (q * f) . x = FALSE ) )