let S be RealNormSpace; :: thesis: for p being Element of S
for r being Real holds cl_Ball (p,r) = { y where y is Point of S : ||.(y - p).|| <= r }
let p be Element of S; :: thesis: for r being Real holds cl_Ball (p,r) = { y where y is Point of S : ||.(y - p).|| <= r }
let r be Real; :: thesis: cl_Ball (p,r) = { y where y is Point of S : ||.(y - p).|| <= r }
deffunc H₁( object ) -> object = $1;
defpred S₁[ Element of S] means ||.(p - $1).|| <= r;
defpred S₂[ Element of S] means ||.($1 - p).|| <= r;
A1: for v being Element of the carrier of S holds
( S₁[v] iff S₂[v] ) by NORMSP_1:7;
{ H₁(y) where y is Element of the carrier of S : S₁[y] } = { H₁(y) where y is Element of the carrier of S : S₂[y] } from FRAENKEL:sch 3(A1);
hence cl_Ball (p,r) = { y where y is Point of S : ||.(y - p).|| <= r } ; :: thesis: verum