theorem :: NOMIN_3:7

for D being non empty set
for p, q, r being PartialPredicate of D st p ||= PP_or (q,r) holds
for d being Element of D st d in dom p & p . d = TRUE & not ( d in dom q & q . d = TRUE ) holds
( d in dom r & r . d = TRUE )