:: deftheorem Def4 defines PPdisjunction PARTPR_1:def 4 :
for D being non empty set
for b₂ being Function of [:(Pr D),(Pr D):],(Pr D) holds
( b₂ = PPdisjunction D iff for p, q being PartialPredicate of D holds
( dom (b₂ . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (b₂ . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b₂ . (p,q)) . d = FALSE ) ) ) ) );