let n be Nat; :: thesis: for A being Subset of (TOP-REAL n) holds UBD A c= A `
let A be Subset of (TOP-REAL n); :: thesis: UBD A c= A `
reconsider D = UBD A as Subset of ((TOP-REAL n) | (A `)) by Th12;
D c= the carrier of ((TOP-REAL n) | (A `)) ;
hence UBD A c= A ` by PRE_TOPC:8; :: thesis: verum