let X be ComplexUnitarySpace; for x, y being Point of X
for r being Real st y in Ball (x,r) holds
y in cl_Ball (x,r)
let x, y be Point of X; for r being Real st y in Ball (x,r) holds
y in cl_Ball (x,r)
let r be Real; ( y in Ball (x,r) implies y in cl_Ball (x,r) )
assume
y in Ball (x,r)
; y in cl_Ball (x,r)
then
||.(x - y).|| <= r
by Th40;
hence
y in cl_Ball (x,r)
; verum