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