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 Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds
for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= 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 Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds
for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r )
assume A1: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B
for r being Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds
for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r
let G be Rain of A,B; :: thesis: for r being Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds
for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r
let r be Real; :: thesis: ( r in DYADIC \/ (right_open_halfline 1) & 0 < r implies for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r )
assume that
A2: r in DYADIC \/ (right_open_halfline 1) and
A3: 0 < r ; :: thesis: for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r
let p be Point of T; :: thesis: ( p in (Tempest G) . r implies (Thunder G) . p <= r )
assume A4: p in (Tempest G) . r ; :: thesis: (Thunder G) . p <= r

per cases ( r in DYADIC or r in right_open_halfline 1 ) by A2, XBOOLE_0:def 3;

suppose A5: r in DYADIC ; :: thesis: (Thunder G) . p <= r

then r in (halfline 0) \/ DYADIC by XBOOLE_0:def 3;
then A6: r in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

now :: thesis: ( ( Rainbow (p,G) = {} & (Thunder G) . p <= r ) or ( Rainbow (p,G) <> {} & (Thunder G) . p <= r ) )

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

case Rainbow (p,G) = {} ; :: thesis: (Thunder G) . p <= r

hence (Thunder G) . p <= r by A3, Def6; :: thesis: verum

end;

case Rainbow (p,G) <> {} ; :: thesis: (Thunder G) . p <= r

then reconsider S = Rainbow (p,G) as non empty Subset of ExtREAL ;
reconsider er = r as R_eal by XXREAL_0:def 1;
for r1 being ExtReal st r1 in S holds
r1 <= er

proof

let r1 be ExtReal; :: thesis: ( r1 in S implies r1 <= er )
assume A7: r1 in S ; :: thesis: r1 <= er
assume A8: not r1 <= er ; :: thesis: contradiction
A9: S c= DYADIC by Th13;
then r1 in DYADIC by A7;
then reconsider p1 = r1 as Real ;

per cases ( inf_number_dyadic r <= inf_number_dyadic p1 or inf_number_dyadic p1 <= inf_number_dyadic r ) ;

suppose A10: inf_number_dyadic r <= inf_number_dyadic p1 ; :: thesis: contradiction

set n = inf_number_dyadic p1;
r in dyadic (inf_number_dyadic p1) by A5, A10, Th6;
then A11: (Tempest G) . r = (G . (inf_number_dyadic p1)) . r by A1, A5, A6, Def4;
reconsider D = G . (inf_number_dyadic p1) as Drizzle of A,B, inf_number_dyadic p1 by A1, Def2;
p1 in (halfline 0) \/ DYADIC by A7, A9, XBOOLE_0:def 3;
then A12: p1 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;
p1 in dyadic (inf_number_dyadic p1) by A7, A9, Th5;
then A13: (Tempest G) . p1 = (G . (inf_number_dyadic p1)) . p1 by A1, A7, A9, A12, Def4;
reconsider r = r, p1 = p1 as Element of dyadic (inf_number_dyadic p1) by A5, A7, A9, A10, Th6;
( Cl (D . r) c= D . p1 & D . r c= Cl (D . r) ) by A1, A8, Def1, PRE_TOPC:18;
then D . r c= D . p1 ;
hence contradiction by A4, A7, A11, A13, Def5; :: thesis: verum

end;

suppose inf_number_dyadic p1 <= inf_number_dyadic r ; :: thesis: contradiction

then A14: dyadic (inf_number_dyadic p1) c= dyadic (inf_number_dyadic r) by URYSOHN2:29;
set n = inf_number_dyadic r;
reconsider D = G . (inf_number_dyadic r) as Drizzle of A,B, inf_number_dyadic r by A1, Def2;
A15: p1 in dyadic (inf_number_dyadic p1) by A7, A9, Th5;
p1 in (halfline 0) \/ DYADIC by A7, A9, XBOOLE_0:def 3;
then p1 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;
then A16: (Tempest G) . p1 = (G . (inf_number_dyadic r)) . p1 by A1, A7, A9, A15, A14, Def4;
r in dyadic (inf_number_dyadic r) by A5, Th6;
then A17: (Tempest G) . r = (G . (inf_number_dyadic r)) . r by A1, A5, A6, Def4;
reconsider p1 = p1 as Element of dyadic (inf_number_dyadic r) by A15, A14;
reconsider r = r as Element of dyadic (inf_number_dyadic r) by A5, Th6;
( Cl (D . r) c= D . p1 & D . r c= Cl (D . r) ) by A1, A8, Def1, PRE_TOPC:18;
then D . r c= D . p1 ;
hence contradiction by A4, A7, A17, A16, Def5; :: thesis: verum

end;

end;

end;

then r is UpperBound of S by XXREAL_2:def 1;
then sup S <= er by XXREAL_2:def 3;
hence (Thunder G) . p <= r by Def6; :: thesis: verum

end;

end;

end;

hence (Thunder G) . p <= r ; :: thesis: verum

end;

suppose r in right_open_halfline 1 ; :: thesis: (Thunder G) . p <= r

then A18: 1 < r by XXREAL_1:235;

now :: thesis: ( ( Rainbow (p,G) = {} & (Thunder G) . p <= r ) or ( Rainbow (p,G) <> {} & (Thunder G) . p <= r ) )

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

case Rainbow (p,G) = {} ; :: thesis: (Thunder G) . p <= r

hence (Thunder G) . p <= r by A18, Def6; :: thesis: verum

end;

case A19: Rainbow (p,G) <> {} ; :: thesis: (Thunder G) . p <= r

reconsider e1 = 1 as R_eal by XXREAL_0:def 1;
consider S being non empty Subset of ExtREAL such that
A20: S = Rainbow (p,G) by A19;
( sup S <= e1 & (Thunder G) . p = sup S ) by A20, Def6, Th14;
hence (Thunder G) . p <= r by A18, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence (Thunder G) . p <= r ; :: thesis: verum

end;

end;