let X be non empty TopStruct ; :: thesis:
let g be Function of X,R^1; :: thesis:
let B be Subset of X; :: thesis:
let a be Real; :: thesis:
assume that
A1: g is continuous and
A2: B = { p where p is Point of X : g /. p < a } ; :: thesis:
{ r where r is Real : r < a } c= the carrier of R^1

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { r where r is Real : r < a } ; :: thesis:
then consider r being Real such that
A3: ( r = x & r < a ) ;
r in REAL by XREAL_0:def 1;
hence x in the carrier of R^1 by A3, TOPMETR:17; :: thesis:

end;

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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A5: x in g " D ; :: thesis:
then reconsider p = x as Point of X ;
g . x in D by A5, FUNCT_1:def 7;
then A6: ex r being Real st
( r = g . x & r < a ) ;
g /. p = g . p ;
hence x in B by A2, A6; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in B ; :: thesis:
then consider p being Point of X such that
A8: p = x and
A9: g /. p < a by A2;
( dom g = the carrier of X & g . x in D ) by A8, A9, FUNCT_2:def 1;
hence x in g " D by A8, FUNCT_1:def 7; :: thesis:

end;