let T be non empty TopSpace; :: thesis: for f being Function of R^1,T holds

( f is open iff for p being Point of R^1

for r being positive Real ex V being open Subset of T st

( f . p in V & V c= f .: ].(p - r),(p + r).[ ) )

let f be Function of R^1,T; :: thesis: ( f is open iff for p being Point of R^1

for r being positive Real ex V being open Subset of T st

( f . p in V & V c= f .: ].(p - r),(p + r).[ ) )

thus ( f is open implies for p being Point of R^1

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: ].(p - r),(p + r).[ ) ) :: thesis: ( ( for p being Point of R^1

for r being positive Real ex V being open Subset of T st

( f . p in V & V c= f .: ].(p - r),(p + r).[ ) ) implies f is open )

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: ].(p - r),(p + r).[ ) ; :: thesis: f is open

for p being Point of RealSpace

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) )

( f is open iff for p being Point of R^1

for r being positive Real ex V being open Subset of T st

( f . p in V & V c= f .: ].(p - r),(p + r).[ ) )

let f be Function of R^1,T; :: thesis: ( f is open iff for p being Point of R^1

for r being positive Real ex V being open Subset of T st

( f . p in V & V c= f .: ].(p - r),(p + r).[ ) )

thus ( f is open implies for p being Point of R^1

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: ].(p - r),(p + r).[ ) ) :: thesis: ( ( for p being Point of R^1

for r being positive Real ex V being open Subset of T st

( f . p in V & V c= f .: ].(p - r),(p + r).[ ) ) implies f is open )

proof

assume A3:
for p being Point of R^1
assume A1:
f is open
; :: thesis: for p being Point of R^1

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: ].(p - r),(p + r).[ )

let p be Point of R^1; :: thesis: for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: ].(p - r),(p + r).[ )

let r be positive Real; :: thesis: ex W being open Subset of T st

( f . p in W & W c= f .: ].(p - r),(p + r).[ )

reconsider q = p as Point of RealSpace ;

consider W being open Subset of T such that

A2: ( f . p in W & W c= f .: (Ball (q,r)) ) by A1, Th5;

].(q - r),(q + r).[ = Ball (q,r) by FRECHET:7;

hence ex W being open Subset of T st

( f . p in W & W c= f .: ].(p - r),(p + r).[ ) by A2; :: thesis: verum

end;for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: ].(p - r),(p + r).[ )

let p be Point of R^1; :: thesis: for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: ].(p - r),(p + r).[ )

let r be positive Real; :: thesis: ex W being open Subset of T st

( f . p in W & W c= f .: ].(p - r),(p + r).[ )

reconsider q = p as Point of RealSpace ;

consider W being open Subset of T such that

A2: ( f . p in W & W c= f .: (Ball (q,r)) ) by A1, Th5;

].(q - r),(q + r).[ = Ball (q,r) by FRECHET:7;

hence ex W being open Subset of T st

( f . p in W & W c= f .: ].(p - r),(p + r).[ ) by A2; :: thesis: verum

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: ].(p - r),(p + r).[ ) ; :: thesis: f is open

for p being Point of RealSpace

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) )

proof

hence
f is open
by Th5; :: thesis: verum
let p be Point of RealSpace; :: thesis: for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) )

let r be positive Real; :: thesis: ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) )

reconsider q = p as Point of R^1 ;

consider W being open Subset of T such that

A4: ( f . q in W & W c= f .: ].(p - r),(p + r).[ ) by A3;

].(p - r),(p + r).[ = Ball (p,r) by FRECHET:7;

hence ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) by A4; :: thesis: verum

end;( f . p in W & W c= f .: (Ball (p,r)) )

let r be positive Real; :: thesis: ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) )

reconsider q = p as Point of R^1 ;

consider W being open Subset of T such that

A4: ( f . q in W & W c= f .: ].(p - r),(p + r).[ ) by A3;

].(p - r),(p + r).[ = Ball (p,r) by FRECHET:7;

hence ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) by A4; :: thesis: verum