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 \/ & 0 < r holds
for p being Point of T st p in () . r holds
() . 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 \/ & 0 < r holds
for p being Point of T st p in () . r holds
() . p <= r )

assume A1: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B
for r being Real st r in DYADIC \/ & 0 < r holds
for p being Point of T st p in () . r holds
() . p <= r

let G be Rain of A,B; :: thesis: for r being Real st r in DYADIC \/ & 0 < r holds
for p being Point of T st p in () . r holds
() . p <= r

let r be Real; :: thesis: ( r in DYADIC \/ & 0 < r implies for p being Point of T st p in () . r holds
() . p <= r )

assume that
A2: r in DYADIC \/ and
A3: 0 < r ; :: thesis: for p being Point of T st p in () . r holds
() . p <= r

let p be Point of T; :: thesis: ( p in () . r implies () . p <= r )
assume A4: p in () . r ; :: thesis: () . p <= r
per cases by ;
suppose A5: r in DYADIC ; :: thesis: () . p <= r
then r in () \/ DYADIC by XBOOLE_0:def 3;
then A6: r in DOM by ;
now :: thesis: ( ( Rainbow (p,G) = {} & () . p <= r ) or ( Rainbow (p,G) <> {} & () . p <= r ) )
per cases ( Rainbow (p,G) = {} or Rainbow (p,G) <> {} ) ;
case Rainbow (p,G) = {} ; :: thesis: () . p <= r
hence (Thunder G) . p <= r by ; :: thesis: verum
end;
case Rainbow (p,G) <> {} ; :: thesis: () . 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 ;
suppose A10: inf_number_dyadic r <= inf_number_dyadic p1 ; :: thesis: contradiction
set n = inf_number_dyadic p1;
r in dyadic () by A5, A10, Th6;
then A11: (Tempest G) . r = (G . ()) . r by A1, A5, A6, Def4;
reconsider D = G . () as Drizzle of A,B, inf_number_dyadic p1 by ;
p1 in () \/ DYADIC by ;
then A12: p1 in DOM by ;
p1 in dyadic () by A7, A9, Th5;
then A13: (Tempest G) . p1 = (G . ()) . p1 by A1, A7, A9, A12, Def4;
reconsider r = r, p1 = p1 as Element of dyadic () by A5, A7, A9, A10, Th6;
( Cl (D . r) c= D . p1 & D . r c= Cl (D . r) ) by ;
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 () c= dyadic by URYSOHN2:29;
set n = inf_number_dyadic r;
reconsider D = G . as Drizzle of A,B, inf_number_dyadic r by ;
A15: p1 in dyadic () by A7, A9, Th5;
p1 in () \/ DYADIC by ;
then p1 in DOM by ;
then A16: (Tempest G) . p1 = (G . ) . p1 by A1, A7, A9, A15, A14, Def4;
r in dyadic by ;
then A17: (Tempest G) . r = (G . ) . r by A1, A5, A6, Def4;
reconsider p1 = p1 as Element of dyadic by ;
reconsider r = r as Element of dyadic by ;
( Cl (D . r) c= D . p1 & D . r c= Cl (D . r) ) by ;
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: () . p <= r
then A18: 1 < r by XXREAL_1:235;
now :: thesis: ( ( Rainbow (p,G) = {} & () . p <= r ) or ( Rainbow (p,G) <> {} & () . p <= r ) )
per cases ( Rainbow (p,G) = {} or Rainbow (p,G) <> {} ) ;
case Rainbow (p,G) = {} ; :: thesis: () . p <= r
hence (Thunder G) . p <= r by ; :: thesis: verum
end;
case A19: Rainbow (p,G) <> {} ; :: thesis: () . 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 & () . p = sup S ) by ;
hence (Thunder G) . p <= r by ; :: thesis: verum
end;
end;
end;
hence (Thunder G) . p <= r ; :: thesis: verum
end;
end;