theorem Th16: :: PARTPR_1:16

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