consider A being trivial Subset of (TOP-REAL n);
A is Subset of (TOP-REAL n) ;
hence ex b₁ being Subset of (TOP-REAL n) st b₁ is trivial ; :: thesis: verum