for n being Nat st n >= 1 holds
BDD ({} (TOP-REAL n)) = {} (TOP-REAL n)