:: deftheorem Def12 defines PartialPredConnectivesJoin PARTPR_1:def 12 :
for D being non empty set
for b₂ being BinOp of (Pr D) holds
( b₂ = PartialPredConnectivesJoin D iff for p, q being PartialPredicate of D holds b₂ . (p,q) = PP_or (p,q) );