let S be compact Subset of (TOP-REAL 2); :: thesis: proj1 .: S is compact

proj1 .: S is closed by Th3;

hence proj1 .: S is compact by JORDAN1C:3, RCOMP_1:11; :: thesis: verum

proj1 .: S is closed by Th3;

hence proj1 .: S is compact by JORDAN1C:3, RCOMP_1:11; :: thesis: verum