let S be compact Subset of (TOP-REAL 2); :: thesis: proj2 .: S is compact
proj2 .: S is closed by Th13;
hence proj2 .: S is compact by Th14, RCOMP_1:11; :: thesis: verum