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