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