theorem Th31: :: PARTPR_1:31

for D being non empty set
for p, q being PartialPredicate of D holds dom (PP_imp (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) }