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