let S be compact Subset of (TOP-REAL 2); :: thesis: proj1 .: S is compact
A1: ( S is Bounded & S is closed ) by JORDAN2C:73;
then proj1 .: S is closed by Th3;
hence proj1 .: S is compact by A1, JORDAN1C:4, RCOMP_1:29; :: thesis: verum