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 Th89; :: according to XBOOLE_0:def 10 :: thesis: proj2 .: (Cl P) c= Cl (proj2 .: P)
thus proj2 .: (Cl P) c= Cl (proj2 .: P) by Th91; :: thesis: verum