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