let S be closed Subset of (TOP-REAL 2); :: thesis: ( S is Bounded implies proj1 .: S is closed )
assume S is Bounded ; :: thesis: proj1 .: S is closed
then Cl (proj1 .: S) = proj1 .: (Cl S) by TOPREAL6:92
.= proj1 .: S by PRE_TOPC:52 ;
hence proj1 .: S is closed ; :: thesis: verum