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 3, XBOOLE_0:def 3;

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 3, 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;

end;

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:1;

hence C is open ; :: thesis: verum

end;then C in the topology of T by PRE_TOPC:1;

hence C is open ; :: thesis: verum

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 A1, Def2;

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 A1, Def1;

A8: (Tempest G) . r = (G . n) . r by A1, A3, A5, A6, Def4;

end;A6: r in dyadic n by URYSOHN1:def 2;

reconsider D = G . n as Drizzle of A,B,n by A1, Def2;

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 A1, Def1;

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 ) )

hence
C is open
; :: thesis: verumend;