let P be Subset of (TOP-REAL 2); :: thesis: ( P is Bounded implies Cl (proj1 .: P) = proj1 .: (Cl P) )
assume P is Bounded ; :: thesis: Cl (proj1 .: P) = proj1 .: (Cl P)
hence Cl (proj1 .: P) c= proj1 .: (Cl P) by Th89; :: according to XBOOLE_0:def 10 :: thesis: proj1 .: (Cl P) c= Cl (proj1 .: P)
thus proj1 .: (Cl P) c= Cl (proj1 .: P) by Th90; :: thesis: verum