let X be RealNormSpace; :: thesis: for r being Real

for x being Point of X holds { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r }

let r be Real; :: thesis: for x being Point of X holds { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r }

let x be Point of X; :: thesis: { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r }

hence { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r } by A3, XBOOLE_0:def 10; :: thesis: verum

for x being Point of X holds { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r }

let r be Real; :: thesis: for x being Point of X holds { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r }

let x be Point of X; :: thesis: { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r }

now :: thesis: for s being object st s in { y where y is Point of X : ||.(y - x).|| < r } holds

s in { y where y is Point of X : ||.(x - y).|| < r }

then A3:
{ y where y is Point of X : ||.(y - x).|| < r } c= { y where y is Point of X : ||.(x - y).|| < r }
;s in { y where y is Point of X : ||.(x - y).|| < r }

let s be object ; :: thesis: ( s in { y where y is Point of X : ||.(y - x).|| < r } implies s in { y where y is Point of X : ||.(x - y).|| < r } )

assume s in { y where y is Point of X : ||.(y - x).|| < r } ; :: thesis: s in { y where y is Point of X : ||.(x - y).|| < r }

then consider z being Point of X such that

A1: s = z and

A2: ||.(z - x).|| < r ;

||.(x - z).|| < r by A2, NORMSP_1:7;

hence s in { y where y is Point of X : ||.(x - y).|| < r } by A1; :: thesis: verum

end;assume s in { y where y is Point of X : ||.(y - x).|| < r } ; :: thesis: s in { y where y is Point of X : ||.(x - y).|| < r }

then consider z being Point of X such that

A1: s = z and

A2: ||.(z - x).|| < r ;

||.(x - z).|| < r by A2, NORMSP_1:7;

hence s in { y where y is Point of X : ||.(x - y).|| < r } by A1; :: thesis: verum

now :: thesis: for s being object st s in { y where y is Point of X : ||.(x - y).|| < r } holds

s in { y where y is Point of X : ||.(y - x).|| < r }

then
{ y where y is Point of X : ||.(x - y).|| < r } c= { y where y is Point of X : ||.(y - x).|| < r }
;s in { y where y is Point of X : ||.(y - x).|| < r }

let s be object ; :: thesis: ( s in { y where y is Point of X : ||.(x - y).|| < r } implies s in { y where y is Point of X : ||.(y - x).|| < r } )

assume s in { y where y is Point of X : ||.(x - y).|| < r } ; :: thesis: s in { y where y is Point of X : ||.(y - x).|| < r }

then consider z being Point of X such that

A4: s = z and

A5: ||.(x - z).|| < r ;

||.(z - x).|| < r by A5, NORMSP_1:7;

hence s in { y where y is Point of X : ||.(y - x).|| < r } by A4; :: thesis: verum

end;assume s in { y where y is Point of X : ||.(x - y).|| < r } ; :: thesis: s in { y where y is Point of X : ||.(y - x).|| < r }

then consider z being Point of X such that

A4: s = z and

A5: ||.(x - z).|| < r ;

||.(z - x).|| < r by A5, NORMSP_1:7;

hence s in { y where y is Point of X : ||.(y - x).|| < r } by A4; :: thesis: verum

hence { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r } by A3, XBOOLE_0:def 10; :: thesis: verum