take Ball ( the Point of (TOP-REAL n), the Real) ; :: thesis: Ball ( the Point of (TOP-REAL n), the Real) is ball
thus Ball ( the Point of (TOP-REAL n), the Real) is ball ; :: thesis: verum