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 A2: ( r in DYADIC \/ (right_open_halfline 1) & 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 A3: 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 A4: r in DYADIC ; :: thesis: (Thunder G) . p <= r

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

now

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

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

hence (Thunder G) . p <= r by A2, 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 ext-real number st r1 in S holds
r1 <= er

proof

let r1 be ext-real number ; :: thesis: ( r1 in S implies r1 <= er )
assume A6: r1 in S ; :: thesis: r1 <= er
A7: S c= DYADIC by Th15;
then r1 in DYADIC by A6;
then reconsider p1 = r1 as Real ;
assume A8: not r1 <= er ; :: thesis: contradiction

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

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

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

end;

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

set n = inf_number_dyadic r;
A15: p1 in dyadic (inf_number_dyadic p1) by A6, A7, Th6;
A16: dyadic (inf_number_dyadic p1) c= dyadic (inf_number_dyadic r) by A14, URYSOHN2:33;
r in dyadic (inf_number_dyadic r) by A4, Th7;
then A17: (Tempest G) . r = (G . (inf_number_dyadic r)) . r by A1, A4, A5, Def4;
p1 in (halfline 0 ) \/ DYADIC by A6, A7, XBOOLE_0:def 3;
then p1 in DOM by URYSOHN1:def 5, XBOOLE_0:def 3;
then A18: (Tempest G) . p1 = (G . (inf_number_dyadic r)) . p1 by A1, A6, A7, A15, A16, Def4;
reconsider D = G . (inf_number_dyadic r) as Drizzle of A,B, inf_number_dyadic r by A1, Def2;
reconsider r = r as Element of dyadic (inf_number_dyadic r) by A4, Th7;
reconsider p1 = p1 as Element of dyadic (inf_number_dyadic r) by A15, A16;
A19: Cl (D . r) c= D . p1 by A1, A8, Def1;
D . r c= Cl (D . r) by PRE_TOPC:48;
then D . r c= D . p1 by A19, XBOOLE_1:1;
hence contradiction by A3, A6, A17, A18, 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 A20: 1 < r by XXREAL_1:235;

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

end;