:: deftheorem defines PPisEmpty PARTPR_2:def 8 :
for D being set
for b₂ being PartialPredicate of D holds
( b₂ = PPisEmpty D iff ( dom b₂ = D & ( for d being object st d in dom b₂ holds
( ( d = {} implies b₂ . d = TRUE ) & ( d <> {} implies b₂ . d = FALSE ) ) ) ) );