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