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 = (Tempest G) . 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 = (Tempest G) . 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 = (Tempest G) . 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 = (Tempest G) . r & r in DOM holds
C is open
let r be Real; :: thesis: for C being Subset of T st C = (Tempest G) . r & r in DOM holds
C is open
let C be Subset of T; :: thesis: ( C = (Tempest G) . r & r in DOM implies C is open )
assume that
A2: C = (Tempest G) . r and
A3: r in DOM ; :: thesis: C is open
A4: ( r in (halfline 0 ) \/ DYADIC or r in right_open_halfline 1 ) by A3, URYSOHN1:def 5, XBOOLE_0:def 3;

per cases ( r in halfline 0 or r in DYADIC or r in right_open_halfline 1 ) by A4, XBOOLE_0:def 3;

suppose r in halfline 0 ; :: thesis: C is open

then C = {} by A1, A2, A3, Def4;
then C in the topology of T by PRE_TOPC:5;
hence C is open by PRE_TOPC:def 5; :: thesis: verum

end;

suppose A5: r in DYADIC ; :: thesis: C is open

then consider n being Element of NAT such that
A6: r in dyadic n by URYSOHN1:def 4;
A7: (Tempest G) . r = (G . n) . r by A1, A3, A5, A6, Def4;
reconsider D = G . n as Drizzle of A,B,n by A1, Def2;
A8: 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 A1, Def1;

now

per cases ( r = 0 or 0 < r ) by A6, URYSOHN1:5;

case A9: r = 0 ; :: thesis: C is open

then A10: ( 1 is Element of dyadic n & r is Element of dyadic n & r < 1 ) by URYSOHN1:12;
reconsider r = r as Element of dyadic n by A9, URYSOHN1:12;
D . r = C by A1, A2, A3, A5, Def4;
hence C is open by A1, A10, Def1; :: thesis: verum

end;

case 0 < r ; :: thesis: C is open

then ( 0 in dyadic n & 0 < r ) by URYSOHN1:12;
hence C is open by A2, A6, A7, A8; :: thesis: verum

end;

end;

end;

hence C is open ; :: thesis: verum

end;

suppose r in right_open_halfline 1 ; :: thesis: C is open

then A11: C = the carrier of T by A1, A2, A3, Def4;
the carrier of T in the topology of T by PRE_TOPC:def 1;
hence C is open by A11, PRE_TOPC:def 5; :: thesis: verum

end;

end;