for n being Nat
for A being Subset of (TOP-REAL n) holds (BDD A) \/ (UBD A) = A `