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 Element of DOM
for p being Point of T st (Thunder G) . p < r holds
p in (Tempest G) . 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 Element of DOM
for p being Point of T st (Thunder G) . p < r holds
p in (Tempest G) . r )
assume A1: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B
for r being Element of DOM
for p being Point of T st (Thunder G) . p < r holds
p in (Tempest G) . r
let G be Rain of A,B; :: thesis: for r being Element of DOM
for p being Point of T st (Thunder G) . p < r holds
p in (Tempest G) . r
let r be Element of DOM ; :: thesis: for p being Point of T st (Thunder G) . p < r holds
p in (Tempest G) . r
let p be Point of T; :: thesis: ( (Thunder G) . p < r implies p in (Tempest G) . r )
assume A2: (Thunder G) . p < r ; :: thesis: p in (Tempest G) . r
now :: thesis: ( not p in (Tempest G) . r implies p in (Tempest G) . r )
per cases ( Rainbow (p,G) = {} or Rainbow (p,G) <> {} ) ;
suppose A3: Rainbow (p,G) = {} ; :: thesis: ( not p in (Tempest G) . r implies p in (Tempest G) . r )
assume A4: not p in (Tempest G) . r ; :: thesis: p in (Tempest G) . r
( r in (halfline 0) \/ DYADIC or r in right_open_halfline 1 ) by URYSOHN1:def 3, XBOOLE_0:def 3;
then A5: ( r in halfline 0 or r in DYADIC or r in right_open_halfline 1 ) by XBOOLE_0:def 3;
A6: 0 < r by A2, A3, Def6;
now :: thesis: p in (Tempest G) . r
per cases ( r in DYADIC or r in right_open_halfline 1 ) by A6, A5, XXREAL_1:233;
suppose A7: r in DYADIC ; :: thesis: p in (Tempest G) . r
reconsider r1 = r as R_eal by XXREAL_0:def 1;
A8: for s being Real st s = r1 holds
not p in (Tempest G) . s by A4;
then reconsider S = Rainbow (p,G) as non empty Subset of ExtREAL by A7, Def5;
A9: (Thunder G) . p = sup S by Def6;
r1 in Rainbow (p,G) by A7, A8, Def5;
hence p in (Tempest G) . r by A2, A9, XXREAL_2:4; :: thesis: verum
end;
end;
end;
hence p in (Tempest G) . r ; :: thesis: verum
end;
suppose Rainbow (p,G) <> {} ; :: thesis: ( not p in (Tempest G) . r implies p in (Tempest G) . r )
then reconsider S = Rainbow (p,G) as non empty Subset of ExtREAL ;
reconsider e1 = 1 as R_eal by XXREAL_0:def 1;
consider s being object such that
A10: s in S by XBOOLE_0:def 1;
reconsider s = s as R_eal by A10;
A11: s <= sup S by A10, XXREAL_2:4;
assume A12: not p in (Tempest G) . r ; :: thesis: p in (Tempest G) . r
( r in (halfline 0) \/ DYADIC or r in right_open_halfline 1 ) by URYSOHN1:def 3, XBOOLE_0:def 3;
then A13: ( r in halfline 0 or r in DYADIC or r in right_open_halfline 1 ) by XBOOLE_0:def 3;
A14: (Thunder G) . p = sup S by Def6;
for x being R_eal st x in S holds
( 0. <= x & x <= e1 )
proof
let x be R_eal; :: thesis: ( x in S implies ( 0. <= x & x <= e1 ) )
assume x in S ; :: thesis: ( 0. <= x & x <= e1 )
then A15: x in DYADIC by Def5;
then reconsider x = x as Real ;
ex n being Nat st x in dyadic n by A15, URYSOHN1:def 2;
hence ( 0. <= x & x <= e1 ) by URYSOHN1:1; :: thesis: verum
end;
then A16: 0. <= s by A10;
hence p in (Tempest G) . r ; :: thesis: verum
end;
end;
end;
hence p in (Tempest G) . r ; :: thesis: verum