:: deftheorem defines ||= NOMIN_3:def 3 :
for D being set
for p, q being PartialPredicate of D holds
( p ||= q iff for d being Element of D st d in dom p & p . d = TRUE holds
( d in dom q & q . d = TRUE ) );