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, r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds
for C being Subset of T st C = () . r1 holds
Cl C c= () . r2

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for G being Rain of A,B
for r1, r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds
for C being Subset of T st C = () . r1 holds
Cl C c= () . r2 )

assume A1: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B
for r1, r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds
for C being Subset of T st C = () . r1 holds
Cl C c= () . r2

let G be Rain of A,B; :: thesis: for r1, r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds
for C being Subset of T st C = () . r1 holds
Cl C c= () . r2

let r1, r2 be Real; :: thesis: ( r1 in DOM & r2 in DOM & r1 < r2 implies for C being Subset of T st C = () . r1 holds
Cl C c= () . r2 )

assume that
A2: r1 in DOM and
A3: r2 in DOM and
A4: r1 < r2 ; :: thesis: for C being Subset of T st C = () . r1 holds
Cl C c= () . r2

A5: ( r1 in () \/ DYADIC or r1 in right_open_halfline 1 ) by ;
A6: ( r2 in () \/ DYADIC or r2 in right_open_halfline 1 ) by ;
let C be Subset of T; :: thesis: ( C = () . r1 implies Cl C c= () . r2 )
assume A7: C = () . r1 ; :: thesis: Cl C c= () . r2
per cases ( ( r1 in halfline 0 & r2 in halfline 0 ) or ( r1 in DYADIC & r2 in halfline 0 ) or ( r1 in right_open_halfline 1 & r2 in halfline 0 ) or ( r1 in halfline 0 & r2 in DYADIC ) or ( r1 in DYADIC & r2 in DYADIC ) or ( r1 in right_open_halfline 1 & r2 in DYADIC ) or ( r1 in halfline 0 & r2 in right_open_halfline 1 ) or ( r1 in DYADIC & r2 in right_open_halfline 1 ) or ( r1 in right_open_halfline 1 & r2 in right_open_halfline 1 ) ) by ;
suppose A8: ( r1 in halfline 0 & r2 in halfline 0 ) ; :: thesis: Cl C c= () . r2
C = {} by A1, A2, A7, A8, Def4;
then Cl C = {} by PRE_TOPC:22;
hence Cl C c= () . r2 ; :: thesis: verum
end;
suppose ( r1 in DYADIC & r2 in halfline 0 ) ; :: thesis: Cl C c= () . r2
then ( r2 < 0 & ex s being Nat st r1 in dyadic s ) by ;
hence Cl C c= () . r2 by ; :: thesis: verum
end;
suppose A9: ( r1 in right_open_halfline 1 & r2 in halfline 0 ) ; :: thesis: Cl C c= () . r2
then 1 < r1 by XXREAL_1:235;
hence Cl C c= () . r2 by ; :: thesis: verum
end;
suppose A10: ( r1 in halfline 0 & r2 in DYADIC ) ; :: thesis: Cl C c= () . r2
C = {} by A1, A2, A7, A10, Def4;
then Cl C = {} by PRE_TOPC:22;
hence Cl C c= () . r2 ; :: thesis: verum
end;
suppose A11: ( r1 in DYADIC & r2 in DYADIC ) ; :: thesis: Cl C c= () . r2
then consider n2 being Nat such that
A12: r2 in dyadic n2 by URYSOHN1:def 2;
consider n1 being Nat such that
A13: r1 in dyadic n1 by ;
set n = n1 + n2;
A14: dyadic n1 c= dyadic (n1 + n2) by ;
then A15: (Tempest G) . r1 = (G . (n1 + n2)) . r1 by A1, A2, A11, A13, Def4;
dyadic n2 c= dyadic (n1 + n2) by ;
then reconsider r1 = r1, r2 = r2 as Element of dyadic (n1 + n2) by ;
reconsider D = G . (n1 + n2) as Drizzle of A,B,n1 + n2 by ;
Cl (D . r1) c= D . r2 by A1, A4, Def1;
hence Cl C c= () . r2 by A1, A3, A7, A11, A15, Def4; :: thesis: verum
end;
suppose A16: ( r1 in right_open_halfline 1 & r2 in DYADIC ) ; :: thesis: Cl C c= () . r2
end;
suppose A18: ( r1 in halfline 0 & r2 in right_open_halfline 1 ) ; :: thesis: Cl C c= () . r2
C = {} by A1, A2, A7, A18, Def4;
then Cl C = {} by PRE_TOPC:22;
hence Cl C c= () . r2 ; :: thesis: verum
end;
suppose ( r1 in DYADIC & r2 in right_open_halfline 1 ) ; :: thesis: Cl C c= () . r2
then (Tempest G) . r2 = the carrier of T by A1, A3, Def4;
hence Cl C c= () . r2 ; :: thesis: verum
end;
suppose ( r1 in right_open_halfline 1 & r2 in right_open_halfline 1 ) ; :: thesis: Cl C c= () . r2
then (Tempest G) . r2 = the carrier of T by A1, A3, Def4;
hence Cl C c= () . r2 ; :: thesis: verum
end;
end;