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 ;
].(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