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:83
.= proj1 .: S by PRE_TOPC:22 ;
hence proj1 .: S is closed ; :: thesis: verum