take cl_Ball ((0. (TOP-REAL n)),1) ; :: thesis: ( not cl_Ball ((0. (TOP-REAL n)),1) is empty & cl_Ball ((0. (TOP-REAL n)),1) is closed & cl_Ball ((0. (TOP-REAL n)),1) is convex & cl_Ball ((0. (TOP-REAL n)),1) is bounded )
thus ( not cl_Ball ((0. (TOP-REAL n)),1) is empty & cl_Ball ((0. (TOP-REAL n)),1) is closed & cl_Ball ((0. (TOP-REAL n)),1) is convex & cl_Ball ((0. (TOP-REAL n)),1) is bounded ) ; :: thesis: verum