let m be Nat; :: thesis: for f being Function of (),R^1 holds
( f is open iff for p being Point of ()
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 (),R^1; :: thesis: ( f is open iff for p being Point of ()
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 ()
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 ()
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 (); :: 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 ;
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 ;
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 ()
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 (); :: 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 () such that
A8: p in A and
A9: x = f . p by FUNCT_2:65;
reconsider u = p as Point of () by EUCLID:67;
A = Int A by ;
then consider e being Real such that
A10: e > 0 and
A11: Ball (u,e) c= A by ;
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 ;
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 ;
hence Q c= f .: A by A13; :: thesis: x in Q
thus x in Q by ; :: 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