theorem :: JORDAN1K:16

for n being Nat holds BDD ([#] (TOP-REAL n)) = {} (TOP-REAL n)