let P be Subset of (TOP-REAL 2); :: thesis: ( P is bounded implies Cl (proj2 .: P) = proj2 .: (Cl P) )
assume P is bounded ; :: thesis: Cl (proj2 .: P) = proj2 .: (Cl P)
hence Cl (proj2 .: P) c= proj2 .: (Cl P) by Th80; :: according to XBOOLE_0:def 10 :: thesis: proj2 .: (Cl P) c= Cl (proj2 .: P)
thus proj2 .: (Cl P) c= Cl (proj2 .: P) by Th82; :: thesis: verum