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
for C being Subset of T st C = () . r & r in DOM holds
C is open

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
for C being Subset of T st C = () . r & r in DOM holds
C is open )

assume A1: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B
for r being Real
for C being Subset of T st C = () . r & r in DOM holds
C is open

let G be Rain of A,B; :: thesis: for r being Real
for C being Subset of T st C = () . r & r in DOM holds
C is open

let r be Real; :: thesis: for C being Subset of T st C = () . r & r in DOM holds
C is open

let C be Subset of T; :: thesis: ( C = () . r & r in DOM implies C is open )
assume that
A2: C = () . r and
A3: r in DOM ; :: thesis: C is open
A4: ( r in () \/ DYADIC or r in right_open_halfline 1 ) by ;
per cases by ;
suppose r in halfline 0 ; :: thesis: C is open
end;
suppose A5: r in DYADIC ; :: thesis: C is open
then consider n being Nat such that
A6: r in dyadic n by URYSOHN1:def 2;
reconsider D = G . n as Drizzle of A,B,n by ;
A7: for r1, r2 being Element of dyadic n st r1 < r2 holds
( D . r1 is open & D . r2 is open & Cl (D . r1) c= D . r2 & A c= D . 0 & B = ([#] T) \ (D . 1) ) by ;
A8: (Tempest G) . r = (G . n) . r by A1, A3, A5, A6, Def4;
now :: thesis: ( ( r = 0 & C is open ) or ( 0 < r & C is open ) )
per cases ( r = 0 or 0 < r ) by ;
case A9: r = 0 ; :: thesis: C is open
then reconsider r = r as Element of dyadic n by URYSOHN1:6;
( 1 is Element of dyadic n & D . r = C ) by ;
hence C is open by A1, A9, Def1; :: thesis: verum
end;
end;
end;
hence C is open ; :: thesis: verum
end;
suppose A11: r in right_open_halfline 1 ; :: thesis: C is open
A12: the carrier of T in the topology of T by PRE_TOPC:def 1;
C = the carrier of T by A1, A2, A3, A11, Def4;
hence C is open by A12; :: thesis: verum
end;
end;