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

now

per cases ( Rainbow p,G = {} or Rainbow p,G <> {} ) ;

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

then A3: 0 < r by A2, Def6;
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 5, 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;

now

per cases ( r in DYADIC or r in right_open_halfline 1 ) by A3, A5, XXREAL_1:233;

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

reconsider r1 = r as R_eal by XXREAL_0:def 1;
A7: for s being Real st s = r1 holds
not p in (Tempest G) . s by A4;
then A8: r1 in Rainbow p,G by A6, Def5;
reconsider S = Rainbow p,G as non empty Subset of ExtREAL by A6, A7, Def5;
(Thunder G) . p = sup S by Def6;
hence p in (Tempest G) . r by A2, A8, XXREAL_2:4; :: thesis: verum

end;

suppose r in right_open_halfline 1 ; :: thesis: p in (Tempest G) . r

then (Tempest G) . r = the carrier of T by A1, Def4;
hence p in (Tempest G) . r ; :: thesis: verum

end;

end;

end;

hence p in (Tempest G) . r ; :: thesis: verum

end;

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 ;
A9: (Thunder G) . p = sup S by Def6;
reconsider e1 = 1 as R_eal by XXREAL_0:def 1;
A10: for x being R_eal st x in S holds
( 0. <= x & x <= e1 )

proof

let x be R_eal; :: thesis: ( x in S implies ( 0. <= x & x <= e1 ) )
assume x in S ; :: thesis: ( 0. <= x & x <= e1 )
then A11: x in DYADIC by Def5;
then reconsider x = x as Real ;
consider n being Element of NAT such that
A12: x in dyadic n by A11, URYSOHN1:def 4;
thus ( 0. <= x & x <= e1 ) by A12, URYSOHN1:5; :: thesis: verum

end;

consider s being set such that
A13: s in S by XBOOLE_0:def 1;
reconsider s = s as R_eal by A13;
A14: ( 0. <= s & s <= sup S ) by A10, A13, XXREAL_2:4;
assume A15: 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 5, XBOOLE_0:def 3;
then A16: ( r in halfline 0 or r in DYADIC or r in right_open_halfline 1 ) by XBOOLE_0:def 3;

now

per cases ( r in DYADIC or r in right_open_halfline 1 ) by A2, A9, A14, A16, XXREAL_1:233;

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

reconsider r1 = r as R_eal by XXREAL_0:def 1;
for s being Real st s = r1 holds
not p in (Tempest G) . s by A15;
then r1 in Rainbow p,G by A17, Def5;
hence p in (Tempest G) . r by A2, A9, XXREAL_2:4; :: thesis: verum

end;

suppose r in right_open_halfline 1 ; :: thesis: p in (Tempest G) . r

then (Tempest G) . r = the carrier of T by A1, Def4;
hence p in (Tempest G) . r ; :: thesis: verum

end;

end;

end;

hence p in (Tempest G) . r ; :: thesis: verum

end;

end;

end;

hence p in (Tempest G) . r ; :: thesis: verum