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 r1 being Element of DOM st 0 < r1 holds

for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for G being Rain of A,B

for r1 being Element of DOM st 0 < r1 holds

for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1 )

assume A1: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B

for r1 being Element of DOM st 0 < r1 holds

for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1

let G be Rain of A,B; :: thesis: for r1 being Element of DOM st 0 < r1 holds

for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1

let r1 be Element of DOM ; :: thesis: ( 0 < r1 implies for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1 )

assume A2: 0 < r1 ; :: thesis: for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1

let p be Point of T; :: thesis: ( r1 < (Thunder G) . p implies not p in (Tempest G) . r1 )

assume A3: ( r1 < (Thunder G) . p & p in (Tempest G) . r1 ) ; :: thesis: contradiction

( r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 ) by URYSOHN1:def 3, XBOOLE_0:def 3;

then ( r1 in halfline 0 or r1 in DYADIC or r1 in right_open_halfline 1 ) by XBOOLE_0:def 3;

then r1 in DYADIC \/ (right_open_halfline 1) by A2, XBOOLE_0:def 3, XXREAL_1:233;

hence contradiction by A1, A2, A3, Th16; :: thesis: verum

for G being Rain of A,B

for r1 being Element of DOM st 0 < r1 holds

for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for G being Rain of A,B

for r1 being Element of DOM st 0 < r1 holds

for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1 )

assume A1: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B

for r1 being Element of DOM st 0 < r1 holds

for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1

let G be Rain of A,B; :: thesis: for r1 being Element of DOM st 0 < r1 holds

for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1

let r1 be Element of DOM ; :: thesis: ( 0 < r1 implies for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1 )

assume A2: 0 < r1 ; :: thesis: for p being Point of T st r1 < (Thunder G) . p holds

not p in (Tempest G) . r1

let p be Point of T; :: thesis: ( r1 < (Thunder G) . p implies not p in (Tempest G) . r1 )

assume A3: ( r1 < (Thunder G) . p & p in (Tempest G) . r1 ) ; :: thesis: contradiction

( r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 ) by URYSOHN1:def 3, XBOOLE_0:def 3;

then ( r1 in halfline 0 or r1 in DYADIC or r1 in right_open_halfline 1 ) by XBOOLE_0:def 3;

then r1 in DYADIC \/ (right_open_halfline 1) by A2, XBOOLE_0:def 3, XXREAL_1:233;

hence contradiction by A1, A2, A3, Th16; :: thesis: verum