theorem :: JCT_MISC:15

for S being compact Subset of (TOP-REAL 2) holds proj2 .: S is compact