let m be Nat; :: thesis: for f being Function of (TOP-REAL m),R^1 holds
( f is open iff for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) )
let f be Function of (TOP-REAL m),R^1; :: thesis: ( f is open iff for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) )
A1: m in NAT by ORDINAL1:def 12;

hereby :: thesis: ( ( for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ) implies f is open )

assume A2: f is open ; :: thesis: for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))
let p be Point of (TOP-REAL m); :: thesis: for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))
let r be positive Real; :: thesis: ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))
p in Ball (p,r) by A1, TOPGEN_5:13;
then A3: f . p in f .: (Ball (p,r)) by FUNCT_2:35;
f .: (Ball (p,r)) is open by A2;
then consider s being Real such that
A4: s > 0 and
A5: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) by A3, FRECHET:8;
reconsider s = s as positive Real by A4;
take s = s; :: thesis: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))
thus ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) by A5; :: thesis: verum

end;

assume A6: for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ; :: thesis: f is open
let A be Subset of (TOP-REAL m); :: according to T_0TOPSP:def 2 :: thesis: ( not A is open or f .: A is open )
assume A7: A is open ; :: thesis: f .: A is open
for x being set holds
( x in f .: A iff ex Q being Subset of R^1 st
( Q is open & Q c= f .: A & x in Q ) )

proof

let x be set ; :: thesis: ( x in f .: A iff ex Q being Subset of R^1 st
( Q is open & Q c= f .: A & x in Q ) )

hereby :: thesis: ( ex Q being Subset of R^1 st
( Q is open & Q c= f .: A & x in Q ) implies x in f .: A )

assume x in f .: A ; :: thesis: ex Q being Element of K16( the U1 of K409()) st
( Q is open & Q c= f .: A & x in Q )
then consider p being Point of (TOP-REAL m) such that
A8: p in A and
A9: x = f . p by FUNCT_2:65;
reconsider u = p as Point of (Euclid m) by EUCLID:67;
A = Int A by A7, TOPS_1:23;
then consider e being Real such that
A10: e > 0 and
A11: Ball (u,e) c= A by A8, GOBOARD6:5;
A12: Ball (u,e) = Ball (p,e) by TOPREAL9:13;
consider s being positive Real such that
A13: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,e)) by A6, A10;
take Q = R^1 ].((f . p) - s),((f . p) + s).[; :: thesis: ( Q is open & Q c= f .: A & x in Q )
thus Q is open ; :: thesis: ( Q c= f .: A & x in Q )
f .: (Ball (p,e)) c= f .: A by A11, A12, RELAT_1:123;
hence Q c= f .: A by A13; :: thesis: x in Q
thus x in Q by A9, TOPREAL6:15; :: thesis: verum

end;

thus ( ex Q being Subset of R^1 st
( Q is open & Q c= f .: A & x in Q ) implies x in f .: A ) ; :: thesis: verum

end;

hence f .: A is open by TOPS_1:25; :: thesis: verum