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 = (Tempest G) . r1 holds
Cl C c= (Tempest G) . 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 = (Tempest G) . r1 holds
Cl C c= (Tempest G) . 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 = (Tempest G) . r1 holds
Cl C c= (Tempest G) . 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 = (Tempest G) . r1 holds
Cl C c= (Tempest G) . r2
let r1, r2 be Real; :: thesis: ( r1 in DOM & r2 in DOM & r1 < r2 implies for C being Subset of T st C = (Tempest G) . r1 holds
Cl C c= (Tempest G) . r2 )
assume A2: ( r1 in DOM & r2 in DOM & r1 < r2 ) ; :: thesis: for C being Subset of T st C = (Tempest G) . r1 holds
Cl C c= (Tempest G) . r2
then A3: ( ( r1 in (halfline 0 ) \/ DYADIC or r1 in right_open_halfline 1 ) & ( r2 in (halfline 0 ) \/ DYADIC or r2 in right_open_halfline 1 ) ) by URYSOHN1:def 5, XBOOLE_0:def 3;
let C be Subset of T; :: thesis: ( C = (Tempest G) . r1 implies Cl C c= (Tempest G) . r2 )
assume A4: C = (Tempest G) . r1 ; :: thesis: Cl C c= (Tempest G) . 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 A3, XBOOLE_0:def 3;

suppose ( r1 in halfline 0 & r2 in halfline 0 ) ; :: thesis: Cl C c= (Tempest G) . r2

then A5: C = {} by A1, A2, A4, Def4;
{} T is closed ;
then Cl C = {} by A5, PRE_TOPC:52;
hence Cl C c= (Tempest G) . r2 by XBOOLE_1:2; :: thesis: verum

end;

suppose A6: ( r1 in DYADIC & r2 in halfline 0 ) ; :: thesis: Cl C c= (Tempest G) . r2

then A7: r2 < 0 by XXREAL_1:233;
consider s being Element of NAT such that
A8: r1 in dyadic s by A6, URYSOHN1:def 4;
thus Cl C c= (Tempest G) . r2 by A2, A7, A8, URYSOHN1:5; :: thesis: verum

end;

suppose A9: ( r1 in right_open_halfline 1 & r2 in halfline 0 ) ; :: thesis: Cl C c= (Tempest G) . r2

then 1 < r1 by XXREAL_1:235;
hence Cl C c= (Tempest G) . r2 by A2, A9, XXREAL_1:233; :: thesis: verum

end;

suppose ( r1 in halfline 0 & r2 in DYADIC ) ; :: thesis: Cl C c= (Tempest G) . r2

then A10: C = {} by A1, A2, A4, Def4;
{} T is closed ;
then Cl C = {} by A10, PRE_TOPC:52;
hence Cl C c= (Tempest G) . r2 by XBOOLE_1:2; :: thesis: verum

end;

suppose A11: ( r1 in DYADIC & r2 in DYADIC ) ; :: thesis: Cl C c= (Tempest G) . r2

then consider n1 being Element of NAT such that
A12: r1 in dyadic n1 by URYSOHN1:def 4;
consider n2 being Element of NAT such that
A13: r2 in dyadic n2 by A11, URYSOHN1:def 4;
set n = n1 + n2;
A14: ( dyadic n1 c= dyadic (n1 + n2) & dyadic n2 c= dyadic (n1 + n2) ) by NAT_1:11, URYSOHN2:33;
then A15: (Tempest G) . r1 = (G . (n1 + n2)) . r1 by A1, A2, A11, A12, Def4;
reconsider D = G . (n1 + n2) as Drizzle of A,B,n1 + n2 by A1, Def2;
reconsider r1 = r1, r2 = r2 as Element of dyadic (n1 + n2) by A12, A13, A14;
Cl (D . r1) c= D . r2 by A1, A2, Def1;
hence Cl C c= (Tempest G) . r2 by A1, A2, A4, A11, A15, Def4; :: thesis: verum

end;

suppose A16: ( r1 in right_open_halfline 1 & r2 in DYADIC ) ; :: thesis: Cl C c= (Tempest G) . r2

then A17: 1 < r1 by XXREAL_1:235;
consider s being Element of NAT such that
A18: r2 in dyadic s by A16, URYSOHN1:def 4;
r2 <= 1 by A18, URYSOHN1:5;
hence Cl C c= (Tempest G) . r2 by A2, A17, XXREAL_0:2; :: thesis: verum

end;

suppose ( r1 in halfline 0 & r2 in right_open_halfline 1 ) ; :: thesis: Cl C c= (Tempest G) . r2

then A19: C = {} by A1, A2, A4, Def4;
{} T is closed ;
then Cl C = {} by A19, PRE_TOPC:52;
hence Cl C c= (Tempest G) . r2 by XBOOLE_1:2; :: thesis: verum

end;

suppose ( r1 in DYADIC & r2 in right_open_halfline 1 ) ; :: thesis: Cl C c= (Tempest G) . r2

then (Tempest G) . r2 = the carrier of T by A1, A2, Def4;
hence Cl C c= (Tempest G) . r2 ; :: thesis: verum

end;

suppose ( r1 in right_open_halfline 1 & r2 in right_open_halfline 1 ) ; :: thesis: Cl C c= (Tempest G) . r2

then (Tempest G) . r2 = the carrier of T by A1, A2, Def4;
hence Cl C c= (Tempest G) . r2 ; :: thesis: verum

end;

end;