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 )

proof

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;

assume A3: 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: 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

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;

hence f is open by Th5; :: thesis: verum