let T be non empty normal TopSpace; 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; ( 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 )
; 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; 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; ( 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
; for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r
let p be Point of T; ( p in (Tempest G) . r implies (Thunder G) . p <= r )
assume A4:
p in (Tempest G) . r
; (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
;
(Thunder G) . p <= rthen
r in (halfline 0) \/ DYADIC
by XBOOLE_0:def 3;
then A6:
r in DOM
by URYSOHN1:def 3, XBOOLE_0:def 3;
now ( ( 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)
<> {}
;
(Thunder G) . p <= rthen 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;
( r1 in S implies r1 <= er )
assume A7:
r1 in S
;
r1 <= er
assume A8:
not
r1 <= er
;
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
;
contradictionset 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;
verum end; suppose
inf_number_dyadic p1 <= inf_number_dyadic r
;
contradictionthen 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;
verum 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;
verum end; hence
(Thunder G) . p <= r
;
verum end;