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 }

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 }

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;

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

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 }

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;

then { y where y is Point of X : ||.(x - y).|| < r } c= { 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