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

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;

end;

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;

end;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 ) )end;

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

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

then sup S <= er by XXREAL_2:def 3;

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

end;reconsider er = r as R_eal by XXREAL_0:def 1;

for r1 being ExtReal st r1 in S holds

r1 <= er

proof

then
r is UpperBound of S
by XXREAL_2:def 1;
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 ;

end;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 )
;

end;

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;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

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;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

then sup S <= er by XXREAL_2:def 3;

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

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

then A18:
1 < r
by XXREAL_1:235;

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

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

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;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