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