let S be closed Subset of (TOP-REAL 2); :: thesis: ( S is bounded implies proj2 .: S is closed )
assume S is bounded ; :: thesis: proj2 .: S is closed
then Cl (proj2 .: S) = proj2 .: (Cl S) by TOPREAL6:84
.= proj2 .: S by PRE_TOPC:22 ;
hence proj2 .: S is closed ; :: thesis: verum