let S be compact Subset of ; :: thesis: proj2 .: S is compact
proj2 .: S is closed by Th22;
hence proj2 .: S is compact by Th23, RCOMP_1:29; :: thesis: verum