set A = the non empty compact Subset of (TOP-REAL n);
reconsider T = (TOP-REAL n) | the non empty compact Subset of (TOP-REAL n) as non empty SubSpace of TOP-REAL n ;
T is compact ;
hence ex b₁ being SubSpace of TOP-REAL n st
( b₁ is compact & not b₁ is empty & b₁ is strict ) ; :: thesis: verum