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