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 < () . p holds
not p in () . 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 < () . p holds
not p in () . 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 < () . p holds
not p in () . 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 < () . p holds
not p in () . r1

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

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

let p be Point of T; :: thesis: ( r1 < () . p implies not p in () . r1 )
assume A3: ( r1 < () . p & p in () . r1 ) ; :: thesis: contradiction
( r1 in () \/ DYADIC or r1 in right_open_halfline 1 ) by ;
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 \/ by ;
hence contradiction by A1, A2, A3, Th16; :: thesis: verum