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 ;
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 ;
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 ; :: thesis: verum