let X be non empty TopStruct ; :: thesis: for g being Function of X,R^1
for B being Subset of X
for a being Real st g is continuous & B = { p where p is Point of X : pi g,p < a } holds
B is open
let g be Function of X,R^1 ; :: thesis: for B being Subset of X
for a being Real st g is continuous & B = { p where p is Point of X : pi g,p < a } holds
B is open
let B be Subset of X; :: thesis: for a being Real st g is continuous & B = { p where p is Point of X : pi g,p < a } holds
B is open
let a be Real; :: thesis: ( g is continuous & B = { p where p is Point of X : pi g,p < a } implies B is open )
assume A1: ( g is continuous & B = { p where p is Point of X : pi g,p < a } ) ; :: thesis: B is open
A2: [#] R^1 <> {} ;
{ r where r is Real : r < a } c= the carrier of R^1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { r where r is Real : r < a } or x in the carrier of R^1 )
assume x in { r where r is Real : r < a } ; :: thesis: x in the carrier of R^1
then consider r being Real such that
A3: ( r = x & r < a ) ;
thus x in the carrier of R^1 by A3, TOPMETR:24; :: thesis: verum

end;

then reconsider D = { r where r is Real : r < a } as Subset of R^1 ;
A4: D is open by JORDAN2B:30;
A5: B c= g " D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in g " D )
assume x in B ; :: thesis: x in g " D
then consider p being Point of X such that
A6: ( p = x & pi g,p < a ) by A1;
A7: dom g = the carrier of X by FUNCT_2:def 1;
pi g,p is Real by XREAL_0:def 1;
then ( x in dom g & g . x in D ) by A6, A7;
hence x in g " D by FUNCT_1:def 13; :: thesis: verum

end;

g " D c= B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in g " D or x in B )
assume A8: x in g " D ; :: thesis: x in B
then ( x in dom g & g . x in D ) by FUNCT_1:def 13;
then consider r being Real such that
A9: ( r = g . x & r < a ) ;
reconsider p = x as Point of X by A8;
pi g,p = g . p ;
hence x in B by A1, A9; :: thesis: verum

end;

then B = g " D by A5, XBOOLE_0:def 10;
hence B is open by A1, A2, A4, TOPS_2:55; :: thesis: verum