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:93
.= proj2 .: S by PRE_TOPC:52 ;
hence proj2 .: S is closed ; :: thesis: verum