let T be non empty normal TopSpace; 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; ( 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 )
; 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; 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 ; ( 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
; for p being Point of T st r1 < (Thunder G) . p holds
not p in (Tempest G) . r1
let p be Point of T; ( r1 < (Thunder G) . p implies not p in (Tempest G) . r1 )
assume A3:
( r1 < (Thunder G) . p & p in (Tempest G) . r1 )
; 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; verum