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

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

C = {} by A1, A2, A7, A8, Def4;
then Cl C = {} by PRE_TOPC:22;
hence Cl C c= (Tempest G) . r2 ; :: thesis: verum

end;

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

then ( r2 < 0 & ex s being Nat st r1 in dyadic s ) by URYSOHN1:def 2, XXREAL_1:233;
hence Cl C c= (Tempest G) . r2 by A4, URYSOHN1:1; :: 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 A4, A9, XXREAL_1:233; :: thesis: verum

end;

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

C = {} by A1, A2, A7, A10, Def4;
then Cl C = {} by PRE_TOPC:22;
hence Cl C c= (Tempest G) . r2 ; :: thesis: verum

end;

suppose A11: ( r1 in DYADIC & r2 in DYADIC ) ; :: thesis: Cl C c= (Tempest G) . 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 A11, URYSOHN1:def 2;
set n = n1 + n2;
A14: dyadic n1 c= dyadic (n1 + n2) by NAT_1:11, URYSOHN2:29;
then A15: (Tempest G) . r1 = (G . (n1 + n2)) . r1 by A1, A2, A11, A13, Def4;
dyadic n2 c= dyadic (n1 + n2) by NAT_1:11, URYSOHN2:29;
then reconsider r1 = r1, r2 = r2 as Element of dyadic (n1 + n2) by A13, A12, A14;
reconsider D = G . (n1 + n2) as Drizzle of A,B,n1 + n2 by A1, Def2;
Cl (D . r1) c= D . r2 by A1, A4, Def1;
hence Cl C c= (Tempest G) . 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= (Tempest G) . r2

then ex s being Nat st r2 in dyadic s by URYSOHN1:def 2;
then A17: r2 <= 1 by URYSOHN1:1;
1 < r1 by A16, XXREAL_1:235;
hence Cl C c= (Tempest G) . r2 by A4, A17, XXREAL_0:2; :: thesis: verum

end;

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

C = {} by A1, A2, A7, A18, Def4;
then Cl C = {} by PRE_TOPC:22;
hence Cl C c= (Tempest G) . r2 ; :: 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, A3, 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, A3, Def4;
hence Cl C c= (Tempest G) . r2 ; :: thesis: verum

end;

end;