let n be Element of NAT ; :: thesis: for X, Y being compact Subset of (TOP-REAL n) holds X /\ Y is compact
let X, Y be compact Subset of (TOP-REAL n); :: thesis: X /\ Y is compact
TOP-REAL n is T_2 by SPPOL_1:26;
hence X /\ Y is compact by COMPTS_1:20; :: thesis: verum