let n be Nat; :: thesis: BDD ([#] (TOP-REAL n)) = {} (TOP-REAL n)
BDD ([#] (TOP-REAL n)) c= ([#] (TOP-REAL n)) ` by JORDAN2C:25;
then BDD ([#] (TOP-REAL n)) c= {} (TOP-REAL n) by XBOOLE_1:37;
hence BDD ([#] (TOP-REAL n)) = {} (TOP-REAL n) by XBOOLE_1:3; :: thesis: verum