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

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;

end;

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;then Cl C = {} by PRE_TOPC:22;

hence Cl C c= (Tempest G) . r2 ; :: thesis: verum

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;hence Cl C c= (Tempest G) . r2 by A4, URYSOHN1:1; :: thesis: verum

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;hence Cl C c= (Tempest G) . r2 by A4, A9, XXREAL_1:233; :: thesis: verum

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;then Cl C = {} by PRE_TOPC:22;

hence Cl C c= (Tempest G) . r2 ; :: thesis: verum

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;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

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;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

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;then Cl C = {} by PRE_TOPC:22;

hence Cl C c= (Tempest G) . r2 ; :: thesis: verum