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

for r being Element of DOM

for p being Point of T st (Thunder G) . p < r holds

p in (Tempest G) . r

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

for r being Element of DOM

for p being Point of T st (Thunder G) . p < r holds

p in (Tempest G) . r )

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

for r being Element of DOM

for p being Point of T st (Thunder G) . p < r holds

p in (Tempest G) . r

let G be Rain of A,B; :: thesis: for r being Element of DOM

for p being Point of T st (Thunder G) . p < r holds

p in (Tempest G) . r

let r be Element of DOM ; :: thesis: for p being Point of T st (Thunder G) . p < r holds

p in (Tempest G) . r

let p be Point of T; :: thesis: ( (Thunder G) . p < r implies p in (Tempest G) . r )

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

for G being Rain of A,B

for r being Element of DOM

for p being Point of T st (Thunder G) . p < r holds

p in (Tempest G) . r

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

for r being Element of DOM

for p being Point of T st (Thunder G) . p < r holds

p in (Tempest G) . r )

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

for r being Element of DOM

for p being Point of T st (Thunder G) . p < r holds

p in (Tempest G) . r

let G be Rain of A,B; :: thesis: for r being Element of DOM

for p being Point of T st (Thunder G) . p < r holds

p in (Tempest G) . r

let r be Element of DOM ; :: thesis: for p being Point of T st (Thunder G) . p < r holds

p in (Tempest G) . r

let p be Point of T; :: thesis: ( (Thunder G) . p < r implies p in (Tempest G) . r )

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

now :: thesis: ( not p in (Tempest G) . r implies p in (Tempest G) . r )end;

hence
p in (Tempest G) . r
; :: thesis: verumper cases
( Rainbow (p,G) = {} or Rainbow (p,G) <> {} )
;

end;

suppose A3:
Rainbow (p,G) = {}
; :: thesis: ( not p in (Tempest G) . r implies p in (Tempest G) . r )

assume A4:
not p in (Tempest G) . r
; :: thesis: p in (Tempest G) . r

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

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

A6: 0 < r by A2, A3, Def6;

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

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

A6: 0 < r by A2, A3, Def6;

now :: thesis: p in (Tempest G) . rend;

hence
p in (Tempest G) . r
; :: thesis: verumper cases
( r in DYADIC or r in right_open_halfline 1 )
by A6, A5, XXREAL_1:233;

end;

suppose A7:
r in DYADIC
; :: thesis: p in (Tempest G) . r

reconsider r1 = r as R_eal by XXREAL_0:def 1;

A8: for s being Real st s = r1 holds

not p in (Tempest G) . s by A4;

then reconsider S = Rainbow (p,G) as non empty Subset of ExtREAL by A7, Def5;

A9: (Thunder G) . p = sup S by Def6;

r1 in Rainbow (p,G) by A7, A8, Def5;

hence p in (Tempest G) . r by A2, A9, XXREAL_2:4; :: thesis: verum

end;A8: for s being Real st s = r1 holds

not p in (Tempest G) . s by A4;

then reconsider S = Rainbow (p,G) as non empty Subset of ExtREAL by A7, Def5;

A9: (Thunder G) . p = sup S by Def6;

r1 in Rainbow (p,G) by A7, A8, Def5;

hence p in (Tempest G) . r by A2, A9, XXREAL_2:4; :: thesis: verum

suppose
Rainbow (p,G) <> {}
; :: thesis: ( not p in (Tempest G) . r implies p in (Tempest G) . r )

then reconsider S = Rainbow (p,G) as non empty Subset of ExtREAL ;

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

consider s being object such that

A10: s in S by XBOOLE_0:def 1;

reconsider s = s as R_eal by A10;

A11: s <= sup S by A10, XXREAL_2:4;

assume A12: not p in (Tempest G) . r ; :: thesis: p in (Tempest G) . r

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

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

A14: (Thunder G) . p = sup S by Def6;

for x being R_eal st x in S holds

( 0. <= x & x <= e1 )

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

consider s being object such that

A10: s in S by XBOOLE_0:def 1;

reconsider s = s as R_eal by A10;

A11: s <= sup S by A10, XXREAL_2:4;

assume A12: not p in (Tempest G) . r ; :: thesis: p in (Tempest G) . r

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

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

A14: (Thunder G) . p = sup S by Def6;

for x being R_eal st x in S holds

( 0. <= x & x <= e1 )

proof

then A16:
0. <= s
by A10;
let x be R_eal; :: thesis: ( x in S implies ( 0. <= x & x <= e1 ) )

assume x in S ; :: thesis: ( 0. <= x & x <= e1 )

then A15: x in DYADIC by Def5;

then reconsider x = x as Real ;

ex n being Nat st x in dyadic n by A15, URYSOHN1:def 2;

hence ( 0. <= x & x <= e1 ) by URYSOHN1:1; :: thesis: verum

end;assume x in S ; :: thesis: ( 0. <= x & x <= e1 )

then A15: x in DYADIC by Def5;

then reconsider x = x as Real ;

ex n being Nat st x in dyadic n by A15, URYSOHN1:def 2;

hence ( 0. <= x & x <= e1 ) by URYSOHN1:1; :: thesis: verum

now :: thesis: p in (Tempest G) . rend;

hence
p in (Tempest G) . r
; :: thesis: verumper cases
( r in DYADIC or r in right_open_halfline 1 )
by A2, A14, A16, A11, A13, XXREAL_1:233;

end;