let E be RealNormSpace; :: thesis: for X, Y being Subset of E
for v being Point of E st X is open & Y = { (x - v) where x is Point of E : x in X } holds
Y is open
let X, Y be Subset of E; :: thesis: for v being Point of E st X is open & Y = { (x - v) where x is Point of E : x in X } holds
Y is open
let v be Point of E; :: thesis: ( X is open & Y = { (x - v) where x is Point of E : x in X } implies Y is open )
assume that
A1: X is open and
A2: Y = { (x - v) where x is Point of E : x in X } ; :: thesis: Y is open
set w = - v;
{ (x + (- v)) where x is Point of E : x in X } c= the carrier of E

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { (x + (- v)) where x is Point of E : x in X } or s in the carrier of E )
assume s in { (x + (- v)) where x is Point of E : x in X } ; :: thesis: s in the carrier of E
then ex x being Point of E st
( s = x + (- v) & x in X ) ;
hence s in the carrier of E ; :: thesis: verum

end;

then reconsider Z = { (x + (- v)) where x is Point of E : x in X } as Subset of E ;
deffunc H₁( Point of E) -> Element of the carrier of E = $1 + (- v);
deffunc H₂( Point of E) -> Element of the carrier of E = $1 - v;
defpred S₁[ Point of E] means $1 in X;
A3: for v being Element of the carrier of E holds H₁(v) = H₂(v) ;
{ H₁(v1) where v1 is Element of the carrier of E : S₁[v1] } = { H₂(v2) where v2 is Element of the carrier of E : S₁[v2] } from FRAENKEL:sch 5(A3);
hence Y is open by A1, A2, OP1; :: thesis: verum