A1:
1 in dyadic 0
by TARSKI:def 2, URYSOHN1:2;

then A2: 1 in DYADIC by URYSOHN1:def 2;

then 1 in (halfline 0) \/ DYADIC by XBOOLE_0:def 3;

then A3: 1 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

reconsider e1 = 1 as R_eal by XXREAL_0:def 1;

let T be non empty normal TopSpace; :: thesis: for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B holds

( Thunder G is continuous & ( for x being Point of T holds

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for G being Rain of A,B holds

( Thunder G is continuous & ( for x being Point of T holds

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) ) )

assume A4: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B holds

( Thunder G is continuous & ( for x being Point of T holds

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )

let G be Rain of A,B; :: thesis: ( Thunder G is continuous & ( for x being Point of T holds

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )

A5: 0 in dyadic 0 by TARSKI:def 2, URYSOHN1:2;

then A6: 0 in DYADIC by URYSOHN1:def 2;

then 0 in (halfline 0) \/ DYADIC by XBOOLE_0:def 3;

then A7: 0 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

A8: for x being Point of T holds

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) ) by A8, TMAP_1:44; :: thesis: verum

then A2: 1 in DYADIC by URYSOHN1:def 2;

then 1 in (halfline 0) \/ DYADIC by XBOOLE_0:def 3;

then A3: 1 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

reconsider e1 = 1 as R_eal by XXREAL_0:def 1;

let T be non empty normal TopSpace; :: thesis: for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B holds

( Thunder G is continuous & ( for x being Point of T holds

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for G being Rain of A,B holds

( Thunder G is continuous & ( for x being Point of T holds

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) ) )

assume A4: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B holds

( Thunder G is continuous & ( for x being Point of T holds

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )

let G be Rain of A,B; :: thesis: ( Thunder G is continuous & ( for x being Point of T holds

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )

A5: 0 in dyadic 0 by TARSKI:def 2, URYSOHN1:2;

then A6: 0 in DYADIC by URYSOHN1:def 2;

then 0 in (halfline 0) \/ DYADIC by XBOOLE_0:def 3;

then A7: 0 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

A8: for x being Point of T holds

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )

proof

for p being Point of T holds Thunder G is_continuous_at p
let x be Point of T; :: thesis: ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )

end;now :: thesis: ( ( Rainbow (x,G) = {} & 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) or ( Rainbow (x,G) <> {} & 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) )end;

hence
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )
; :: thesis: verumper cases
( Rainbow (x,G) = {} or Rainbow (x,G) <> {} )
;

end;

case A9:
Rainbow (x,G) = {}
; :: thesis: ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )

( x in B implies (Thunder G) . x = 1 )

end;proof

hence
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )
by A9, Def6; :: thesis: verum
G . 0 is Drizzle of A,B, 0
by A4, Def2;

then A10: B = ([#] T) \ ((G . 0) . 1) by A4, Def1;

assume A11: x in B ; :: thesis: (Thunder G) . x = 1

(Tempest G) . 1 = (G . 0) . 1 by A4, A1, A2, A3, Def4;

then for s being Real st s = 1 holds

not x in (Tempest G) . s by A11, A10, XBOOLE_0:def 5;

hence (Thunder G) . x = 1 by A9, Def5, URYSOHN2:27; :: thesis: verum

end;then A10: B = ([#] T) \ ((G . 0) . 1) by A4, Def1;

assume A11: x in B ; :: thesis: (Thunder G) . x = 1

(Tempest G) . 1 = (G . 0) . 1 by A4, A1, A2, A3, Def4;

then for s being Real st s = 1 holds

not x in (Tempest G) . s by A11, A10, XBOOLE_0:def 5;

hence (Thunder G) . x = 1 by A9, Def5, URYSOHN2:27; :: thesis: verum

case A12:
Rainbow (x,G) <> {}
; :: thesis: ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )

A13:
( x in A implies (Thunder G) . x = 0 )

A29: sup S <= e1 by Th14;

A30: ( x in B implies (Thunder G) . x = 1 )

hence ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) by A13, A30, Th14; :: thesis: verum

end;proof

reconsider S = Rainbow (x,G) as non empty Subset of ExtREAL by A12;
assume A14:
x in A
; :: thesis: (Thunder G) . x = 0

A15: for s being R_eal st 0. < s holds

not s in Rainbow (x,G)

then A24: A c= (G . 0) . 0 by A4, Def1;

A25: (Tempest G) . 0 = (G . 0) . 0 by A4, A5, A6, A7, Def4;

consider a being object such that

A26: a in Rainbow (x,G) by A12, XBOOLE_0:def 1;

A27: a in DYADIC by A26, Def5;

then reconsider a = a as Real ;

A28: ex n being Nat st a in dyadic n by A27, URYSOHN1:def 2;

end;A15: for s being R_eal st 0. < s holds

not s in Rainbow (x,G)

proof

G . 0 is Drizzle of A,B, 0
by A4, Def2;
let s be R_eal; :: thesis: ( 0. < s implies not s in Rainbow (x,G) )

assume 0. < s ; :: thesis: not s in Rainbow (x,G)

assume A16: s in Rainbow (x,G) ; :: thesis: contradiction

then A17: s in DYADIC by Def5;

then reconsider s = s as Real ;

consider n being Nat such that

A18: s in dyadic n by A17, URYSOHN1:def 2;

s in (halfline 0) \/ DYADIC by A17, XBOOLE_0:def 3;

then s in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

then A19: (Tempest G) . s = (G . n) . s by A4, A17, A18, Def4;

reconsider r1 = 0 , r2 = s as Element of dyadic n by A18, URYSOHN1:6;

reconsider D = G . n as Drizzle of A,B,n by A4, Def2;

end;assume 0. < s ; :: thesis: not s in Rainbow (x,G)

assume A16: s in Rainbow (x,G) ; :: thesis: contradiction

then A17: s in DYADIC by Def5;

then reconsider s = s as Real ;

consider n being Nat such that

A18: s in dyadic n by A17, URYSOHN1:def 2;

s in (halfline 0) \/ DYADIC by A17, XBOOLE_0:def 3;

then s in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

then A19: (Tempest G) . s = (G . n) . s by A4, A17, A18, Def4;

reconsider r1 = 0 , r2 = s as Element of dyadic n by A18, URYSOHN1:6;

reconsider D = G . n as Drizzle of A,B,n by A4, Def2;

then A24: A c= (G . 0) . 0 by A4, Def1;

A25: (Tempest G) . 0 = (G . 0) . 0 by A4, A5, A6, A7, Def4;

consider a being object such that

A26: a in Rainbow (x,G) by A12, XBOOLE_0:def 1;

A27: a in DYADIC by A26, Def5;

then reconsider a = a as Real ;

A28: ex n being Nat st a in dyadic n by A27, URYSOHN1:def 2;

A29: sup S <= e1 by Th14;

A30: ( x in B implies (Thunder G) . x = 1 )

proof

( e1 = 1 & (Thunder G) . x = sup S )
by Def6;
G . 0 is Drizzle of A,B, 0
by A4, Def2;

then A31: B = ([#] T) \ ((G . 0) . 1) by A4, Def1;

assume A32: x in B ; :: thesis: (Thunder G) . x = 1

(Tempest G) . 1 = (G . 0) . 1 by A4, A1, A2, A3, Def4;

then A33: for s being Real st s = 1 holds

not x in (Tempest G) . s by A32, A31, XBOOLE_0:def 5;

then reconsider S = Rainbow (x,G) as non empty Subset of ExtREAL by Def5, URYSOHN2:27;

1 in Rainbow (x,G) by A33, Def5, URYSOHN2:27;

then A34: e1 <= sup S by XXREAL_2:4;

(Thunder G) . x = sup S by Def6;

hence (Thunder G) . x = 1 by A29, A34, XXREAL_0:1; :: thesis: verum

end;then A31: B = ([#] T) \ ((G . 0) . 1) by A4, Def1;

assume A32: x in B ; :: thesis: (Thunder G) . x = 1

(Tempest G) . 1 = (G . 0) . 1 by A4, A1, A2, A3, Def4;

then A33: for s being Real st s = 1 holds

not x in (Tempest G) . s by A32, A31, XBOOLE_0:def 5;

then reconsider S = Rainbow (x,G) as non empty Subset of ExtREAL by Def5, URYSOHN2:27;

1 in Rainbow (x,G) by A33, Def5, URYSOHN2:27;

then A34: e1 <= sup S by XXREAL_2:4;

(Thunder G) . x = sup S by Def6;

hence (Thunder G) . x = 1 by A29, A34, XXREAL_0:1; :: thesis: verum

hence ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) by A13, A30, Th14; :: thesis: verum

proof

hence
( Thunder G is continuous & ( for x being Point of T holds
let p be Point of T; :: thesis: Thunder G is_continuous_at p

for Q being Subset of R^1 st Q is open & (Thunder G) . p in Q holds

ex H being Subset of T st

( H is open & p in H & (Thunder G) .: H c= Q )

end;for Q being Subset of R^1 st Q is open & (Thunder G) . p in Q holds

ex H being Subset of T st

( H is open & p in H & (Thunder G) .: H c= Q )

proof

hence
Thunder G is_continuous_at p
by TMAP_1:43; :: thesis: verum
let Q be Subset of R^1; :: thesis: ( Q is open & (Thunder G) . p in Q implies ex H being Subset of T st

( H is open & p in H & (Thunder G) .: H c= Q ) )

assume that

A35: Q is open and

A36: (Thunder G) . p in Q ; :: thesis: ex H being Subset of T st

( H is open & p in H & (Thunder G) .: H c= Q )

reconsider x = (Thunder G) . p as Element of RealSpace by A36, TOPMETR:12, TOPMETR:def 6;

reconsider Q = Q as Subset of REAL by TOPMETR:17;

( the topology of R^1 = Family_open_set RealSpace & Q in the topology of R^1 ) by A35, TOPMETR:12, TOPMETR:def 6;

then consider r being Real such that

A37: r > 0 and

A38: Ball (x,r) c= Q by A36, PCOMPS_1:def 4;

ex r0 being Real st

( r0 < r & 0 < r0 & r0 <= 1 )

A41: r0 < r and

A42: ( 0 < r0 & r0 <= 1 ) ;

consider r1 being Real such that

A43: r1 in DYADIC and

A44: 0 < r1 and

A45: r1 < r0 by A42, URYSOHN2:24;

A46: r1 in DYADIC \/ (right_open_halfline 1) by A43, XBOOLE_0:def 3;

consider n being Nat such that

A47: r1 in dyadic n by A43, URYSOHN1:def 2;

reconsider D = G . n as Drizzle of A,B,n by A4, Def2;

r1 in (halfline 0) \/ DYADIC by A43, XBOOLE_0:def 3;

then A48: r1 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

then A49: (Tempest G) . r1 = (G . n) . r1 by A4, A43, A47, Def4;

A50: r1 < r by A41, A45, XXREAL_0:2;

A51: for p being Point of T st p in (Tempest G) . r1 holds

(Thunder G) . p < r

reconsider r1 = r1 as Element of dyadic n by A47;

reconsider H = D . r1 as Subset of T ;

A53: 0 in dyadic n by URYSOHN1:6;

ex H being Subset of T st

( H is open & p in H & (Thunder G) .: H c= Q )

( H is open & p in H & (Thunder G) .: H c= Q ) ; :: thesis: verum

end;( H is open & p in H & (Thunder G) .: H c= Q ) )

assume that

A35: Q is open and

A36: (Thunder G) . p in Q ; :: thesis: ex H being Subset of T st

( H is open & p in H & (Thunder G) .: H c= Q )

reconsider x = (Thunder G) . p as Element of RealSpace by A36, TOPMETR:12, TOPMETR:def 6;

reconsider Q = Q as Subset of REAL by TOPMETR:17;

( the topology of R^1 = Family_open_set RealSpace & Q in the topology of R^1 ) by A35, TOPMETR:12, TOPMETR:def 6;

then consider r being Real such that

A37: r > 0 and

A38: Ball (x,r) c= Q by A36, PCOMPS_1:def 4;

ex r0 being Real st

( r0 < r & 0 < r0 & r0 <= 1 )

proof
end;

then consider r0 being Real such that per cases
( r <= 1 or 1 < r )
;

end;

suppose A39:
r <= 1
; :: thesis: ex r0 being Real st

( r0 < r & 0 < r0 & r0 <= 1 )

( r0 < r & 0 < r0 & r0 <= 1 )

consider r0 being Real such that

A40: ( 0 < r0 & r0 < r ) by A37, XREAL_1:5;

reconsider r0 = r0 as Real ;

take r0 ; :: thesis: ( r0 < r & 0 < r0 & r0 <= 1 )

thus ( r0 < r & 0 < r0 & r0 <= 1 ) by A39, A40, XXREAL_0:2; :: thesis: verum

end;A40: ( 0 < r0 & r0 < r ) by A37, XREAL_1:5;

reconsider r0 = r0 as Real ;

take r0 ; :: thesis: ( r0 < r & 0 < r0 & r0 <= 1 )

thus ( r0 < r & 0 < r0 & r0 <= 1 ) by A39, A40, XXREAL_0:2; :: thesis: verum

A41: r0 < r and

A42: ( 0 < r0 & r0 <= 1 ) ;

consider r1 being Real such that

A43: r1 in DYADIC and

A44: 0 < r1 and

A45: r1 < r0 by A42, URYSOHN2:24;

A46: r1 in DYADIC \/ (right_open_halfline 1) by A43, XBOOLE_0:def 3;

consider n being Nat such that

A47: r1 in dyadic n by A43, URYSOHN1:def 2;

reconsider D = G . n as Drizzle of A,B,n by A4, Def2;

r1 in (halfline 0) \/ DYADIC by A43, XBOOLE_0:def 3;

then A48: r1 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

then A49: (Tempest G) . r1 = (G . n) . r1 by A4, A43, A47, Def4;

A50: r1 < r by A41, A45, XXREAL_0:2;

A51: for p being Point of T st p in (Tempest G) . r1 holds

(Thunder G) . p < r

proof

A52:
the carrier of R^1 = the carrier of RealSpace
by TOPMETR:12, TOPMETR:def 6;
let p be Point of T; :: thesis: ( p in (Tempest G) . r1 implies (Thunder G) . p < r )

assume p in (Tempest G) . r1 ; :: thesis: (Thunder G) . p < r

then (Thunder G) . p <= r1 by A4, A44, A46, Th16;

hence (Thunder G) . p < r by A50, XXREAL_0:2; :: thesis: verum

end;assume p in (Tempest G) . r1 ; :: thesis: (Thunder G) . p < r

then (Thunder G) . p <= r1 by A4, A44, A46, Th16;

hence (Thunder G) . p < r by A50, XXREAL_0:2; :: thesis: verum

reconsider r1 = r1 as Element of dyadic n by A47;

reconsider H = D . r1 as Subset of T ;

A53: 0 in dyadic n by URYSOHN1:6;

ex H being Subset of T st

( H is open & p in H & (Thunder G) .: H c= Q )

proof
end;

hence
ex H being Subset of T st per cases
( x = 0 or x <> 0 )
;

end;

suppose A54:
x = 0
; :: thesis: ex H being Subset of T st

( H is open & p in H & (Thunder G) .: H c= Q )

( H is open & p in H & (Thunder G) .: H c= Q )

take
H
; :: thesis: ( H is open & p in H & (Thunder G) .: H c= Q )

(Thunder G) .: H c= Q

end;(Thunder G) .: H c= Q

proof

hence
( H is open & p in H & (Thunder G) .: H c= Q )
by A4, A44, A48, A49, A53, A54, Def1, Th15; :: thesis: verum
reconsider p = x as Real ;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Thunder G) .: H or y in Q )

assume y in (Thunder G) .: H ; :: thesis: y in Q

then consider x1 being object such that

x1 in dom (Thunder G) and

A55: x1 in H and

A56: y = (Thunder G) . x1 by FUNCT_1:def 6;

reconsider y = y as Point of RealSpace by A52, A55, A56, FUNCT_2:5;

reconsider q = y as Real ;

A57: - (p - q) < r by A51, A49, A54, A55, A56;

reconsider x1 = x1 as Point of T by A55;

A58: 0 <= (Thunder G) . x1 by A8;

A59: q - p < r - 0 by A51, A49, A54, A55, A56;

then p - q < r by A54, A56, A58, XREAL_1:14;

then A60: |.(p - q).| <> r by A57, ABSVALUE:def 1;

A61: ( dist (x,y) < r implies y in Ball (x,r) ) by METRIC_1:11;

- (- (p - q)) = p - q ;

then - r < p - q by A57, XREAL_1:24;

then ( dist (x,y) = |.(p - q).| & |.(p - q).| <= r ) by A54, A56, A58, A59, ABSVALUE:5, TOPMETR:11;

hence y in Q by A38, A61, A60, XXREAL_0:1; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Thunder G) .: H or y in Q )

assume y in (Thunder G) .: H ; :: thesis: y in Q

then consider x1 being object such that

x1 in dom (Thunder G) and

A55: x1 in H and

A56: y = (Thunder G) . x1 by FUNCT_1:def 6;

reconsider y = y as Point of RealSpace by A52, A55, A56, FUNCT_2:5;

reconsider q = y as Real ;

A57: - (p - q) < r by A51, A49, A54, A55, A56;

reconsider x1 = x1 as Point of T by A55;

A58: 0 <= (Thunder G) . x1 by A8;

A59: q - p < r - 0 by A51, A49, A54, A55, A56;

then p - q < r by A54, A56, A58, XREAL_1:14;

then A60: |.(p - q).| <> r by A57, ABSVALUE:def 1;

A61: ( dist (x,y) < r implies y in Ball (x,r) ) by METRIC_1:11;

- (- (p - q)) = p - q ;

then - r < p - q by A57, XREAL_1:24;

then ( dist (x,y) = |.(p - q).| & |.(p - q).| <= r ) by A54, A56, A58, A59, ABSVALUE:5, TOPMETR:11;

hence y in Q by A38, A61, A60, XXREAL_0:1; :: thesis: verum

suppose A62:
x <> 0
; :: thesis: ex H being Subset of T st

( H is open & p in H & (Thunder G) .: H c= Q )

( H is open & p in H & (Thunder G) .: H c= Q )

reconsider x = x as Real ;

0 <= (Thunder G) . p by A8;

then consider r1, r2 being Real such that

A63: r1 in DYADIC \/ (right_open_halfline 1) and

r2 in DYADIC \/ (right_open_halfline 1) and

A64: 0 < r1 and

A65: r1 < x and

A66: x < r2 and

A67: r2 - r1 < r by A37, A62, URYSOHN2:31;

( r1 in DYADIC or r1 in right_open_halfline 1 ) by A63, XBOOLE_0:def 3;

then ( r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 ) by XBOOLE_0:def 3;

then A68: r1 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

then reconsider B = (Tempest G) . r1 as Subset of T by FUNCT_2:5;

reconsider C = ([#] T) \ (Cl B) as Subset of T ;

consider r3 being Real such that

A69: r3 in DOM and

A70: x < r3 and

A71: r3 < r2 by A66, URYSOHN2:25;

Cl (Cl B) = Cl B ;

then Cl B is closed by PRE_TOPC:22;

then A72: C is open ;

reconsider A = (Tempest G) . r3 as Subset of T by A69, FUNCT_2:5;

take H = A /\ C; :: thesis: ( H is open & p in H & (Thunder G) .: H c= Q )

A73: (Thunder G) .: H c= Q

then consider r4 being Real such that

A87: r4 in DYADIC and

A88: r1 < r4 and

A89: r4 < x by A64, A65, URYSOHN2:24;

A90: r4 in (halfline 0) \/ DYADIC by A87, XBOOLE_0:def 3;

then r4 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

then A91: Cl B c= (Tempest G) . r4 by A4, A88, A68, Th12;

reconsider r4 = r4 as Element of DOM by A90, URYSOHN1:def 3, XBOOLE_0:def 3;

not p in (Tempest G) . r4 by A4, A64, A88, A89, Th17;

then not p in Cl B by A91;

then A92: p in C by XBOOLE_0:def 5;

( A is open & p in (Tempest G) . r3 ) by A4, A69, A70, Th11, Th15;

hence ( H is open & p in H & (Thunder G) .: H c= Q ) by A72, A92, A73, TOPS_1:11, XBOOLE_0:def 4; :: thesis: verum

end;0 <= (Thunder G) . p by A8;

then consider r1, r2 being Real such that

A63: r1 in DYADIC \/ (right_open_halfline 1) and

r2 in DYADIC \/ (right_open_halfline 1) and

A64: 0 < r1 and

A65: r1 < x and

A66: x < r2 and

A67: r2 - r1 < r by A37, A62, URYSOHN2:31;

( r1 in DYADIC or r1 in right_open_halfline 1 ) by A63, XBOOLE_0:def 3;

then ( r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 ) by XBOOLE_0:def 3;

then A68: r1 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

then reconsider B = (Tempest G) . r1 as Subset of T by FUNCT_2:5;

reconsider C = ([#] T) \ (Cl B) as Subset of T ;

consider r3 being Real such that

A69: r3 in DOM and

A70: x < r3 and

A71: r3 < r2 by A66, URYSOHN2:25;

Cl (Cl B) = Cl B ;

then Cl B is closed by PRE_TOPC:22;

then A72: C is open ;

reconsider A = (Tempest G) . r3 as Subset of T by A69, FUNCT_2:5;

take H = A /\ C; :: thesis: ( H is open & p in H & (Thunder G) .: H c= Q )

A73: (Thunder G) .: H c= Q

proof

(Thunder G) . p <= 1
by A8;
reconsider x = x as Element of RealSpace ;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Thunder G) .: H or y in Q )

reconsider p = x as Real ;

assume y in (Thunder G) .: H ; :: thesis: y in Q

then consider x1 being object such that

x1 in dom (Thunder G) and

A74: x1 in H and

A75: y = (Thunder G) . x1 by FUNCT_1:def 6;

reconsider x1 = x1 as Point of T by A74;

A76: x1 in (Tempest G) . r3 by A74, XBOOLE_0:def 4;

reconsider y = y as Real by A75;

reconsider y = y as Point of RealSpace by A52, A74, A75, FUNCT_2:5;

reconsider q = y as Real ;

A77: - (- (p - q)) = p - q ;

A78: not r3 <= 0 by A8, A70;

( r3 in (halfline 0) \/ DYADIC or r3 in right_open_halfline 1 ) by A69, URYSOHN1:def 3, XBOOLE_0:def 3;

then ( r3 in halfline 0 or r3 in DYADIC or r3 in right_open_halfline 1 ) by XBOOLE_0:def 3;

then r3 in DYADIC \/ (right_open_halfline 1) by A78, XBOOLE_0:def 3, XXREAL_1:233;

then (Thunder G) . x1 <= r3 by A4, A76, A78, Th16;

then (Thunder G) . x1 < r2 by A71, XXREAL_0:2;

then A79: q - p < r2 - r1 by A65, A75, XREAL_1:14;

then - (p - q) < r by A67, XXREAL_0:2;

then A80: - r < p - q by A77, XREAL_1:24;

A81: x1 in ([#] T) \ (Cl B) by A74, XBOOLE_0:def 4;

not x1 in B

then p - q < r by A67, XXREAL_0:2;

then A84: ( dist (x,y) = |.(p - q).| & |.(p - q).| <= r ) by A80, ABSVALUE:5, TOPMETR:11;

A85: |.(p - q).| <> r

hence y in Q by A38, A84, A85, XXREAL_0:1; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Thunder G) .: H or y in Q )

reconsider p = x as Real ;

assume y in (Thunder G) .: H ; :: thesis: y in Q

then consider x1 being object such that

x1 in dom (Thunder G) and

A74: x1 in H and

A75: y = (Thunder G) . x1 by FUNCT_1:def 6;

reconsider x1 = x1 as Point of T by A74;

A76: x1 in (Tempest G) . r3 by A74, XBOOLE_0:def 4;

reconsider y = y as Real by A75;

reconsider y = y as Point of RealSpace by A52, A74, A75, FUNCT_2:5;

reconsider q = y as Real ;

A77: - (- (p - q)) = p - q ;

A78: not r3 <= 0 by A8, A70;

( r3 in (halfline 0) \/ DYADIC or r3 in right_open_halfline 1 ) by A69, URYSOHN1:def 3, XBOOLE_0:def 3;

then ( r3 in halfline 0 or r3 in DYADIC or r3 in right_open_halfline 1 ) by XBOOLE_0:def 3;

then r3 in DYADIC \/ (right_open_halfline 1) by A78, XBOOLE_0:def 3, XXREAL_1:233;

then (Thunder G) . x1 <= r3 by A4, A76, A78, Th16;

then (Thunder G) . x1 < r2 by A71, XXREAL_0:2;

then A79: q - p < r2 - r1 by A65, A75, XREAL_1:14;

then - (p - q) < r by A67, XXREAL_0:2;

then A80: - r < p - q by A77, XREAL_1:24;

A81: x1 in ([#] T) \ (Cl B) by A74, XBOOLE_0:def 4;

not x1 in B

proof

then A83:
p - q < r2 - r1
by A4, A66, A68, A75, Th15, XREAL_1:14;
A82:
B c= Cl B
by PRE_TOPC:18;

assume x1 in B ; :: thesis: contradiction

hence contradiction by A81, A82, XBOOLE_0:def 5; :: thesis: verum

end;assume x1 in B ; :: thesis: contradiction

hence contradiction by A81, A82, XBOOLE_0:def 5; :: thesis: verum

then p - q < r by A67, XXREAL_0:2;

then A84: ( dist (x,y) = |.(p - q).| & |.(p - q).| <= r ) by A80, ABSVALUE:5, TOPMETR:11;

A85: |.(p - q).| <> r

proof

( dist (x,y) < r implies y in Ball (x,r) )
by METRIC_1:11;
assume A86:
|.(p - q).| = r
; :: thesis: contradiction

end;hence y in Q by A38, A84, A85, XXREAL_0:1; :: thesis: verum

then consider r4 being Real such that

A87: r4 in DYADIC and

A88: r1 < r4 and

A89: r4 < x by A64, A65, URYSOHN2:24;

A90: r4 in (halfline 0) \/ DYADIC by A87, XBOOLE_0:def 3;

then r4 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

then A91: Cl B c= (Tempest G) . r4 by A4, A88, A68, Th12;

reconsider r4 = r4 as Element of DOM by A90, URYSOHN1:def 3, XBOOLE_0:def 3;

not p in (Tempest G) . r4 by A4, A64, A88, A89, Th17;

then not p in Cl B by A91;

then A92: p in C by XBOOLE_0:def 5;

( A is open & p in (Tempest G) . r3 ) by A4, A69, A70, Th11, Th15;

hence ( H is open & p in H & (Thunder G) .: H c= Q ) by A72, A92, A73, TOPS_1:11, XBOOLE_0:def 4; :: thesis: verum

( H is open & p in H & (Thunder G) .: H c= Q ) ; :: thesis: verum

( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) ) by A8, TMAP_1:44; :: thesis: verum