take Ball ( the Point of (TOP-REAL n), the real number ) ; :: thesis: Ball ( the Point of (TOP-REAL n), the real number ) is ball
thus Ball ( the Point of (TOP-REAL n), the real number ) is ball by Def1; :: thesis: verum