:: deftheorem Def11 defines PartialPredConnectivesMeet PARTPR_1:def 11 :
for D being non empty set
for b₂ being BinOp of (Pr D) holds
( b₂ = PartialPredConnectivesMeet D iff for p, q being PartialPredicate of D holds b₂ . (p,q) = PP_and (p,q) );