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 () . p < r holds
p in () . 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 () . p < r holds
p in () . 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 () . p < r holds
p in () . r

let G be Rain of A,B; :: thesis: for r being Element of DOM
for p being Point of T st () . p < r holds
p in () . r

let r be Element of DOM ; :: thesis: for p being Point of T st () . p < r holds
p in () . r

let p be Point of T; :: thesis: ( () . p < r implies p in () . r )
assume A2: (Thunder G) . p < r ; :: thesis: p in () . r
now :: thesis: ( not p in () . r implies p in () . r )
per cases ( Rainbow (p,G) = {} or Rainbow (p,G) <> {} ) ;
suppose A3: Rainbow (p,G) = {} ; :: thesis: ( not p in () . r implies p in () . r )
assume A4: not p in () . r ; :: thesis: p in () . r
( r in () \/ DYADIC or r in right_open_halfline 1 ) by ;
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 () . r
per cases by ;
suppose A7: r in DYADIC ; :: thesis: p in () . r
reconsider r1 = r as R_eal by XXREAL_0:def 1;
A8: for s being Real st s = r1 holds
not p in () . s by A4;
then reconsider S = Rainbow (p,G) as non empty Subset of ExtREAL by ;
A9: (Thunder G) . p = sup S by Def6;
r1 in Rainbow (p,G) by A7, A8, Def5;
hence p in () . r by ; :: thesis: verum
end;
suppose r in right_open_halfline 1 ; :: thesis: p in () . r
then (Tempest G) . r = the carrier of T by ;
hence p in () . r ; :: thesis: verum
end;
end;
end;
hence p in () . r ; :: thesis: verum
end;
suppose Rainbow (p,G) <> {} ; :: thesis: ( not p in () . r implies p in () . 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 ;
assume A12: not p in () . r ; :: thesis: p in () . r
( r in () \/ DYADIC or r in right_open_halfline 1 ) by ;
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 ;
hence ( 0. <= x & x <= e1 ) by URYSOHN1:1; :: thesis: verum
end;
then A16: 0. <= s by A10;
now :: thesis: p in () . r
per cases by ;
suppose A17: r in DYADIC ; :: thesis: p in () . r
reconsider r1 = r as R_eal by XXREAL_0:def 1;
for s being Real st s = r1 holds
not p in () . s by A12;
then r1 in Rainbow (p,G) by ;
hence p in () . r by ; :: thesis: verum
end;
suppose r in right_open_halfline 1 ; :: thesis: p in () . r
then (Tempest G) . r = the carrier of T by ;
hence p in () . r ; :: thesis: verum
end;
end;
end;
hence p in () . r ; :: thesis: verum
end;
end;
end;
hence p in () . r ; :: thesis: verum