let X be RealUnitarySpace; :: thesis: for x, z being Point of X

for r being Real holds

( z in Ball (x,r) iff dist (x,z) < r )

let x, z be Point of X; :: thesis: for r being Real holds

( z in Ball (x,r) iff dist (x,z) < r )

let r be Real; :: thesis: ( z in Ball (x,r) iff dist (x,z) < r )

thus ( z in Ball (x,r) implies dist (x,z) < r ) :: thesis: ( dist (x,z) < r implies z in Ball (x,r) )

then ||.(x - z).|| < r by BHSP_1:def 5;

hence z in Ball (x,r) ; :: thesis: verum

for r being Real holds

( z in Ball (x,r) iff dist (x,z) < r )

let x, z be Point of X; :: thesis: for r being Real holds

( z in Ball (x,r) iff dist (x,z) < r )

let r be Real; :: thesis: ( z in Ball (x,r) iff dist (x,z) < r )

thus ( z in Ball (x,r) implies dist (x,z) < r ) :: thesis: ( dist (x,z) < r implies z in Ball (x,r) )

proof

assume
dist (x,z) < r
; :: thesis: z in Ball (x,r)
assume
z in Ball (x,r)
; :: thesis: dist (x,z) < r

then ||.(x - z).|| < r by Th40;

hence dist (x,z) < r by BHSP_1:def 5; :: thesis: verum

end;then ||.(x - z).|| < r by Th40;

hence dist (x,z) < r by BHSP_1:def 5; :: thesis: verum

then ||.(x - z).|| < r by BHSP_1:def 5;

hence z in Ball (x,r) ; :: thesis: verum