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