Metamath Proof Explorer


Theorem mblfinlem3

Description: The difference between two sets measurable by the criterion in ismblfin is itself measurable by the same. Corollary 0.3 of Viaclovsky7 p. 3. (Contributed by Brendan Leahy, 25-Mar-2018) (Revised by Brendan Leahy, 13-Jul-2018)

Ref Expression
Assertion mblfinlem3
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) ) -> sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } , RR , < ) = ( vol* ` ( A \ B ) ) )

Proof

Step Hyp Ref Expression
1 ltso
 |-  < Or RR
2 1 a1i
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) ) -> < Or RR )
3 difss
 |-  ( A \ B ) C_ A
4 ovolsscl
 |-  ( ( ( A \ B ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ B ) ) e. RR )
5 3 4 mp3an1
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ B ) ) e. RR )
6 5 3ad2ant1
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) ) -> ( vol* ` ( A \ B ) ) e. RR )
7 vex
 |-  u e. _V
8 eqeq1
 |-  ( y = u -> ( y = ( vol ` b ) <-> u = ( vol ` b ) ) )
9 8 anbi2d
 |-  ( y = u -> ( ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) <-> ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) )
10 9 rexbidv
 |-  ( y = u -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) )
11 7 10 elab
 |-  ( u e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) )
12 simprl
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) -> b C_ ( A \ B ) )
13 ssdifss
 |-  ( A C_ RR -> ( A \ B ) C_ RR )
14 ovolss
 |-  ( ( b C_ ( A \ B ) /\ ( A \ B ) C_ RR ) -> ( vol* ` b ) <_ ( vol* ` ( A \ B ) ) )
15 12 13 14 syl2anr
 |-  ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) ) -> ( vol* ` b ) <_ ( vol* ` ( A \ B ) ) )
16 uniretop
 |-  RR = U. ( topGen ` ran (,) )
17 16 cldss
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> b C_ RR )
18 ovolcl
 |-  ( b C_ RR -> ( vol* ` b ) e. RR* )
19 17 18 syl
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol* ` b ) e. RR* )
20 ovolcl
 |-  ( ( A \ B ) C_ RR -> ( vol* ` ( A \ B ) ) e. RR* )
21 13 20 syl
 |-  ( A C_ RR -> ( vol* ` ( A \ B ) ) e. RR* )
22 xrlenlt
 |-  ( ( ( vol* ` b ) e. RR* /\ ( vol* ` ( A \ B ) ) e. RR* ) -> ( ( vol* ` b ) <_ ( vol* ` ( A \ B ) ) <-> -. ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) )
23 19 21 22 syl2anr
 |-  ( ( A C_ RR /\ b e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( ( vol* ` b ) <_ ( vol* ` ( A \ B ) ) <-> -. ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) )
24 23 adantrr
 |-  ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) ) -> ( ( vol* ` b ) <_ ( vol* ` ( A \ B ) ) <-> -. ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) )
25 id
 |-  ( u = ( vol ` b ) -> u = ( vol ` b ) )
26 dfss4
 |-  ( b C_ RR <-> ( RR \ ( RR \ b ) ) = b )
27 17 26 sylib
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ ( RR \ b ) ) = b )
28 rembl
 |-  RR e. dom vol
29 16 cldopn
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ b ) e. ( topGen ` ran (,) ) )
30 opnmbl
 |-  ( ( RR \ b ) e. ( topGen ` ran (,) ) -> ( RR \ b ) e. dom vol )
31 29 30 syl
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ b ) e. dom vol )
32 difmbl
 |-  ( ( RR e. dom vol /\ ( RR \ b ) e. dom vol ) -> ( RR \ ( RR \ b ) ) e. dom vol )
33 28 31 32 sylancr
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ ( RR \ b ) ) e. dom vol )
34 27 33 eqeltrrd
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> b e. dom vol )
35 mblvol
 |-  ( b e. dom vol -> ( vol ` b ) = ( vol* ` b ) )
36 34 35 syl
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol ` b ) = ( vol* ` b ) )
37 25 36 sylan9eqr
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ u = ( vol ` b ) ) -> u = ( vol* ` b ) )
38 37 breq2d
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ u = ( vol ` b ) ) -> ( ( vol* ` ( A \ B ) ) < u <-> ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) )
39 38 notbid
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ u = ( vol ` b ) ) -> ( -. ( vol* ` ( A \ B ) ) < u <-> -. ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) )
40 39 adantrl
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) -> ( -. ( vol* ` ( A \ B ) ) < u <-> -. ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) )
41 40 adantl
 |-  ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) ) -> ( -. ( vol* ` ( A \ B ) ) < u <-> -. ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) )
42 24 41 bitr4d
 |-  ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) ) -> ( ( vol* ` b ) <_ ( vol* ` ( A \ B ) ) <-> -. ( vol* ` ( A \ B ) ) < u ) )
43 15 42 mpbid
 |-  ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) ) -> -. ( vol* ` ( A \ B ) ) < u )
44 43 rexlimdvaa
 |-  ( A C_ RR -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) -> -. ( vol* ` ( A \ B ) ) < u ) )
45 44 imp
 |-  ( ( A C_ RR /\ E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) -> -. ( vol* ` ( A \ B ) ) < u )
46 11 45 sylan2b
 |-  ( ( A C_ RR /\ u e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } ) -> -. ( vol* ` ( A \ B ) ) < u )
47 46 adantlr
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ u e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } ) -> -. ( vol* ` ( A \ B ) ) < u )
48 47 3ad2antl1
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) ) /\ u e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } ) -> -. ( vol* ` ( A \ B ) ) < u )
49 simplr
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( vol* ` A ) e. RR )
50 resubcl
 |-  ( ( ( vol* ` ( A \ B ) ) e. RR /\ u e. RR ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR )
51 50 adantrr
 |-  ( ( ( vol* ` ( A \ B ) ) e. RR /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR )
52 posdif
 |-  ( ( u e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( u < ( vol* ` ( A \ B ) ) <-> 0 < ( ( vol* ` ( A \ B ) ) - u ) ) )
53 52 ancoms
 |-  ( ( ( vol* ` ( A \ B ) ) e. RR /\ u e. RR ) -> ( u < ( vol* ` ( A \ B ) ) <-> 0 < ( ( vol* ` ( A \ B ) ) - u ) ) )
54 53 biimpd
 |-  ( ( ( vol* ` ( A \ B ) ) e. RR /\ u e. RR ) -> ( u < ( vol* ` ( A \ B ) ) -> 0 < ( ( vol* ` ( A \ B ) ) - u ) ) )
55 54 impr
 |-  ( ( ( vol* ` ( A \ B ) ) e. RR /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> 0 < ( ( vol* ` ( A \ B ) ) - u ) )
56 51 55 elrpd
 |-  ( ( ( vol* ` ( A \ B ) ) e. RR /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR+ )
57 3nn
 |-  3 e. NN
58 nnrp
 |-  ( 3 e. NN -> 3 e. RR+ )
59 57 58 ax-mp
 |-  3 e. RR+
60 rpdivcl
 |-  ( ( ( ( vol* ` ( A \ B ) ) - u ) e. RR+ /\ 3 e. RR+ ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR+ )
61 56 59 60 sylancl
 |-  ( ( ( vol* ` ( A \ B ) ) e. RR /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR+ )
62 5 61 sylan
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR+ )
63 49 62 ltsubrpd
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol* ` A ) )
64 63 adantr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol* ` A ) )
65 simpr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) )
66 64 65 breqtrd
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) )
67 reex
 |-  RR e. _V
68 67 ssex
 |-  ( A C_ RR -> A e. _V )
69 68 adantr
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> A e. _V )
70 sseq1
 |-  ( v = A -> ( v C_ RR <-> A C_ RR ) )
71 fveq2
 |-  ( v = A -> ( vol* ` v ) = ( vol* ` A ) )
72 71 eleq1d
 |-  ( v = A -> ( ( vol* ` v ) e. RR <-> ( vol* ` A ) e. RR ) )
73 70 72 anbi12d
 |-  ( v = A -> ( ( v C_ RR /\ ( vol* ` v ) e. RR ) <-> ( A C_ RR /\ ( vol* ` A ) e. RR ) ) )
74 sseq2
 |-  ( v = A -> ( b C_ v <-> b C_ A ) )
75 74 anbi1d
 |-  ( v = A -> ( ( b C_ v /\ y = ( vol ` b ) ) <-> ( b C_ A /\ y = ( vol ` b ) ) ) )
76 75 rexbidv
 |-  ( v = A -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) ) )
77 76 abbidv
 |-  ( v = A -> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } = { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } )
78 77 sseq1d
 |-  ( v = A -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR <-> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR ) )
79 77 neeq1d
 |-  ( v = A -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) <-> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) ) )
80 77 raleqdv
 |-  ( v = A -> ( A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x <-> A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) )
81 80 rexbidv
 |-  ( v = A -> ( E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x <-> E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) )
82 78 79 81 3anbi123d
 |-  ( v = A -> ( ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) <-> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) ) )
83 73 82 imbi12d
 |-  ( v = A -> ( ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) ) <-> ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) ) ) )
84 simpr
 |-  ( ( b C_ v /\ y = ( vol ` b ) ) -> y = ( vol ` b ) )
85 84 36 sylan9eqr
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ y = ( vol ` b ) ) ) -> y = ( vol* ` b ) )
86 85 adantl
 |-  ( ( ( v C_ RR /\ ( vol* ` v ) e. RR ) /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ y = ( vol ` b ) ) ) ) -> y = ( vol* ` b ) )
87 simprl
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ y = ( vol ` b ) ) ) -> b C_ v )
88 ovolsscl
 |-  ( ( b C_ v /\ v C_ RR /\ ( vol* ` v ) e. RR ) -> ( vol* ` b ) e. RR )
89 88 3expb
 |-  ( ( b C_ v /\ ( v C_ RR /\ ( vol* ` v ) e. RR ) ) -> ( vol* ` b ) e. RR )
90 89 ancoms
 |-  ( ( ( v C_ RR /\ ( vol* ` v ) e. RR ) /\ b C_ v ) -> ( vol* ` b ) e. RR )
91 87 90 sylan2
 |-  ( ( ( v C_ RR /\ ( vol* ` v ) e. RR ) /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ y = ( vol ` b ) ) ) ) -> ( vol* ` b ) e. RR )
92 86 91 eqeltrd
 |-  ( ( ( v C_ RR /\ ( vol* ` v ) e. RR ) /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ y = ( vol ` b ) ) ) ) -> y e. RR )
93 92 rexlimdvaa
 |-  ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) -> y e. RR ) )
94 93 abssdv
 |-  ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR )
95 retop
 |-  ( topGen ` ran (,) ) e. Top
96 0cld
 |-  ( ( topGen ` ran (,) ) e. Top -> (/) e. ( Clsd ` ( topGen ` ran (,) ) ) )
97 95 96 ax-mp
 |-  (/) e. ( Clsd ` ( topGen ` ran (,) ) )
98 0ss
 |-  (/) C_ v
99 0mbl
 |-  (/) e. dom vol
100 mblvol
 |-  ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
101 99 100 ax-mp
 |-  ( vol ` (/) ) = ( vol* ` (/) )
102 ovol0
 |-  ( vol* ` (/) ) = 0
103 101 102 eqtr2i
 |-  0 = ( vol ` (/) )
104 98 103 pm3.2i
 |-  ( (/) C_ v /\ 0 = ( vol ` (/) ) )
105 sseq1
 |-  ( b = (/) -> ( b C_ v <-> (/) C_ v ) )
106 fveq2
 |-  ( b = (/) -> ( vol ` b ) = ( vol ` (/) ) )
107 106 eqeq2d
 |-  ( b = (/) -> ( 0 = ( vol ` b ) <-> 0 = ( vol ` (/) ) ) )
108 105 107 anbi12d
 |-  ( b = (/) -> ( ( b C_ v /\ 0 = ( vol ` b ) ) <-> ( (/) C_ v /\ 0 = ( vol ` (/) ) ) ) )
109 108 rspcev
 |-  ( ( (/) e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( (/) C_ v /\ 0 = ( vol ` (/) ) ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ 0 = ( vol ` b ) ) )
110 97 104 109 mp2an
 |-  E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ 0 = ( vol ` b ) )
111 c0ex
 |-  0 e. _V
112 eqeq1
 |-  ( y = 0 -> ( y = ( vol ` b ) <-> 0 = ( vol ` b ) ) )
113 112 anbi2d
 |-  ( y = 0 -> ( ( b C_ v /\ y = ( vol ` b ) ) <-> ( b C_ v /\ 0 = ( vol ` b ) ) ) )
114 113 rexbidv
 |-  ( y = 0 -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ 0 = ( vol ` b ) ) ) )
115 111 114 spcev
 |-  ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ 0 = ( vol ` b ) ) -> E. y E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) )
116 110 115 ax-mp
 |-  E. y E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) )
117 abn0
 |-  ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) <-> E. y E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) )
118 117 biimpri
 |-  ( E. y E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) -> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) )
119 116 118 mp1i
 |-  ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) )
120 simpr
 |-  ( ( b C_ v /\ z = ( vol ` b ) ) -> z = ( vol ` b ) )
121 120 36 sylan9eqr
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ z = ( vol ` b ) ) ) -> z = ( vol* ` b ) )
122 121 adantl
 |-  ( ( v C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ z = ( vol ` b ) ) ) ) -> z = ( vol* ` b ) )
123 simprl
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ z = ( vol ` b ) ) ) -> b C_ v )
124 ovolss
 |-  ( ( b C_ v /\ v C_ RR ) -> ( vol* ` b ) <_ ( vol* ` v ) )
125 124 ancoms
 |-  ( ( v C_ RR /\ b C_ v ) -> ( vol* ` b ) <_ ( vol* ` v ) )
126 123 125 sylan2
 |-  ( ( v C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ z = ( vol ` b ) ) ) ) -> ( vol* ` b ) <_ ( vol* ` v ) )
127 122 126 eqbrtrd
 |-  ( ( v C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ z = ( vol ` b ) ) ) ) -> z <_ ( vol* ` v ) )
128 127 rexlimdvaa
 |-  ( v C_ RR -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ z = ( vol ` b ) ) -> z <_ ( vol* ` v ) ) )
129 128 alrimiv
 |-  ( v C_ RR -> A. z ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ z = ( vol ` b ) ) -> z <_ ( vol* ` v ) ) )
130 eqeq1
 |-  ( y = z -> ( y = ( vol ` b ) <-> z = ( vol ` b ) ) )
131 130 anbi2d
 |-  ( y = z -> ( ( b C_ v /\ y = ( vol ` b ) ) <-> ( b C_ v /\ z = ( vol ` b ) ) ) )
132 131 rexbidv
 |-  ( y = z -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ z = ( vol ` b ) ) ) )
133 132 ralab
 |-  ( A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ ( vol* ` v ) <-> A. z ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ z = ( vol ` b ) ) -> z <_ ( vol* ` v ) ) )
134 129 133 sylibr
 |-  ( v C_ RR -> A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ ( vol* ` v ) )
135 brralrspcev
 |-  ( ( ( vol* ` v ) e. RR /\ A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ ( vol* ` v ) ) -> E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x )
136 134 135 sylan2
 |-  ( ( ( vol* ` v ) e. RR /\ v C_ RR ) -> E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x )
137 136 ancoms
 |-  ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x )
138 94 119 137 3jca
 |-  ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) )
139 83 138 vtoclg
 |-  ( A e. _V -> ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) ) )
140 69 139 mpcom
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) )
141 140 adantr
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) )
142 62 rpred
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR )
143 49 142 resubcld
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR )
144 suprlub
 |-  ( ( ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) <-> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) )
145 141 143 144 syl2anc
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) <-> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) )
146 145 adantr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) <-> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) )
147 66 146 mpbid
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v )
148 eqeq1
 |-  ( y = v -> ( y = ( vol ` b ) <-> v = ( vol ` b ) ) )
149 148 anbi2d
 |-  ( y = v -> ( ( b C_ A /\ y = ( vol ` b ) ) <-> ( b C_ A /\ v = ( vol ` b ) ) ) )
150 149 rexbidv
 |-  ( y = v -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) ) )
151 150 rexab
 |-  ( E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v <-> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) )
152 breq2
 |-  ( v = ( vol ` b ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v <-> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) )
153 152 ad2antll
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ v = ( vol ` b ) ) ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v <-> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) )
154 sseq1
 |-  ( s = b -> ( s C_ A <-> b C_ A ) )
155 fveq2
 |-  ( s = b -> ( vol ` s ) = ( vol ` b ) )
156 155 breq2d
 |-  ( s = b -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) <-> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) )
157 154 156 anbi12d
 |-  ( s = b -> ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) <-> ( b C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) )
158 157 rspcev
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) )
159 158 expr
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ b C_ A ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) )
160 159 adantrr
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ v = ( vol ` b ) ) ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) )
161 153 160 sylbid
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ v = ( vol ` b ) ) ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) )
162 161 rexlimiva
 |-  ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) )
163 162 imp
 |-  ( ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) )
164 163 exlimiv
 |-  ( E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) )
165 151 164 sylbi
 |-  ( E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) )
166 147 165 syl
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) )
167 166 ex
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) )
168 167 adantlr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) )
169 simplrr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( vol* ` B ) e. RR )
170 62 adantlr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR+ )
171 169 170 ltsubrpd
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol* ` B ) )
172 171 adantr
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol* ` B ) )
173 simpr
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) )
174 172 173 breqtrd
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) )
175 67 ssex
 |-  ( B C_ RR -> B e. _V )
176 175 adantr
 |-  ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> B e. _V )
177 sseq1
 |-  ( v = B -> ( v C_ RR <-> B C_ RR ) )
178 fveq2
 |-  ( v = B -> ( vol* ` v ) = ( vol* ` B ) )
179 178 eleq1d
 |-  ( v = B -> ( ( vol* ` v ) e. RR <-> ( vol* ` B ) e. RR ) )
180 177 179 anbi12d
 |-  ( v = B -> ( ( v C_ RR /\ ( vol* ` v ) e. RR ) <-> ( B C_ RR /\ ( vol* ` B ) e. RR ) ) )
181 sseq2
 |-  ( v = B -> ( b C_ v <-> b C_ B ) )
182 181 anbi1d
 |-  ( v = B -> ( ( b C_ v /\ y = ( vol ` b ) ) <-> ( b C_ B /\ y = ( vol ` b ) ) ) )
183 182 rexbidv
 |-  ( v = B -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) ) )
184 183 abbidv
 |-  ( v = B -> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } = { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } )
185 184 sseq1d
 |-  ( v = B -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR <-> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR ) )
186 184 neeq1d
 |-  ( v = B -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) <-> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) ) )
187 184 raleqdv
 |-  ( v = B -> ( A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x <-> A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) )
188 187 rexbidv
 |-  ( v = B -> ( E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x <-> E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) )
189 185 186 188 3anbi123d
 |-  ( v = B -> ( ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) <-> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) ) )
190 180 189 imbi12d
 |-  ( v = B -> ( ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) ) <-> ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) ) ) )
191 190 138 vtoclg
 |-  ( B e. _V -> ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) ) )
192 176 191 mpcom
 |-  ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) )
193 192 ad2antlr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) )
194 142 adantlr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR )
195 169 194 resubcld
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR )
196 suprlub
 |-  ( ( ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) <-> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) )
197 193 195 196 syl2anc
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) <-> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) )
198 197 adantr
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) <-> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) )
199 174 198 mpbid
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v )
200 148 anbi2d
 |-  ( y = v -> ( ( b C_ B /\ y = ( vol ` b ) ) <-> ( b C_ B /\ v = ( vol ` b ) ) ) )
201 200 rexbidv
 |-  ( y = v -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ v = ( vol ` b ) ) ) )
202 201 rexab
 |-  ( E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v <-> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ v = ( vol ` b ) ) /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) )
203 breq2
 |-  ( v = ( vol ` b ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v <-> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) )
204 203 ad2antll
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ B /\ v = ( vol ` b ) ) ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v <-> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) )
205 sseq1
 |-  ( w = b -> ( w C_ B <-> b C_ B ) )
206 fveq2
 |-  ( w = b -> ( vol ` w ) = ( vol ` b ) )
207 206 breq2d
 |-  ( w = b -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) <-> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) )
208 205 207 anbi12d
 |-  ( w = b -> ( ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) <-> ( b C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) )
209 208 rspcev
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) )
210 209 expr
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ b C_ B ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) )
211 210 adantrr
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ B /\ v = ( vol ` b ) ) ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) )
212 204 211 sylbid
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ B /\ v = ( vol ` b ) ) ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) )
213 212 rexlimiva
 |-  ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ v = ( vol ` b ) ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) )
214 213 imp
 |-  ( ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ v = ( vol ` b ) ) /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) )
215 214 exlimiv
 |-  ( E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ v = ( vol ` b ) ) /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) )
216 202 215 sylbi
 |-  ( E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) )
217 199 216 syl
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) )
218 217 ex
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) )
219 168 218 anim12d
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) )
220 reeanv
 |-  ( E. s e. ( Clsd ` ( topGen ` ran (,) ) ) E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) <-> ( E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) )
221 219 220 syl6ibr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) )
222 eqid
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
223 222 ovolgelb
 |-  ( ( B C_ RR /\ ( vol* ` B ) e. RR /\ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
224 223 3expa
 |-  ( ( ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
225 62 224 sylan2
 |-  ( ( ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
226 225 ancoms
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
227 226 an32s
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
228 elmapi
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
229 ssid
 |-  U. ran ( (,) o. f ) C_ U. ran ( (,) o. f )
230 222 ovollb
 |-  ( ( f : NN --> ( <_ i^i ( RR X. RR ) ) /\ U. ran ( (,) o. f ) C_ U. ran ( (,) o. f ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
231 229 230 mpan2
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
232 231 adantl
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ f : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
233 eqid
 |-  ( ( abs o. - ) o. f ) = ( ( abs o. - ) o. f )
234 233 222 ovolsf
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) )
235 frn
 |-  ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ ( 0 [,) +oo ) )
236 icossxr
 |-  ( 0 [,) +oo ) C_ RR*
237 235 236 sstrdi
 |-  ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* )
238 supxrcl
 |-  ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* )
239 234 237 238 3syl
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* )
240 simpr
 |-  ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` B ) e. RR )
241 readdcl
 |-  ( ( ( vol* ` B ) e. RR /\ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR ) -> ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR )
242 240 142 241 syl2anr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR )
243 242 rexrd
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR* )
244 243 an32s
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR* )
245 rncoss
 |-  ran ( (,) o. f ) C_ ran (,)
246 245 unissi
 |-  U. ran ( (,) o. f ) C_ U. ran (,)
247 unirnioo
 |-  RR = U. ran (,)
248 246 247 sseqtrri
 |-  U. ran ( (,) o. f ) C_ RR
249 ovolcl
 |-  ( U. ran ( (,) o. f ) C_ RR -> ( vol* ` U. ran ( (,) o. f ) ) e. RR* )
250 248 249 ax-mp
 |-  ( vol* ` U. ran ( (,) o. f ) ) e. RR*
251 xrletr
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR* /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* /\ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR* ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
252 250 251 mp3an1
 |-  ( ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* /\ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR* ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
253 239 244 252 syl2anr
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ f : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
254 232 253 mpand
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ f : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
255 228 254 sylan2
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
256 255 anim2d
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) )
257 256 reximdva
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) )
258 227 257 mpd
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
259 rexex
 |-  ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> E. f ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
260 258 259 syl
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> E. f ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
261 16 cldss
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> s C_ RR )
262 indif2
 |-  ( s i^i ( RR \ U. ran ( (,) o. f ) ) ) = ( ( s i^i RR ) \ U. ran ( (,) o. f ) )
263 df-ss
 |-  ( s C_ RR <-> ( s i^i RR ) = s )
264 263 biimpi
 |-  ( s C_ RR -> ( s i^i RR ) = s )
265 264 difeq1d
 |-  ( s C_ RR -> ( ( s i^i RR ) \ U. ran ( (,) o. f ) ) = ( s \ U. ran ( (,) o. f ) ) )
266 262 265 syl5eq
 |-  ( s C_ RR -> ( s i^i ( RR \ U. ran ( (,) o. f ) ) ) = ( s \ U. ran ( (,) o. f ) ) )
267 261 266 syl
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s i^i ( RR \ U. ran ( (,) o. f ) ) ) = ( s \ U. ran ( (,) o. f ) ) )
268 retopbas
 |-  ran (,) e. TopBases
269 bastg
 |-  ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) )
270 268 269 ax-mp
 |-  ran (,) C_ ( topGen ` ran (,) )
271 245 270 sstri
 |-  ran ( (,) o. f ) C_ ( topGen ` ran (,) )
272 uniopn
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ran ( (,) o. f ) C_ ( topGen ` ran (,) ) ) -> U. ran ( (,) o. f ) e. ( topGen ` ran (,) ) )
273 95 271 272 mp2an
 |-  U. ran ( (,) o. f ) e. ( topGen ` ran (,) )
274 16 opncld
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ U. ran ( (,) o. f ) e. ( topGen ` ran (,) ) ) -> ( RR \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
275 95 273 274 mp2an
 |-  ( RR \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) )
276 incld
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( RR \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( s i^i ( RR \ U. ran ( (,) o. f ) ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
277 275 276 mpan2
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s i^i ( RR \ U. ran ( (,) o. f ) ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
278 267 277 eqeltrrd
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
279 278 adantr
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( s \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
280 279 ad2antlr
 |-  ( ( ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( s \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
281 simprll
 |-  ( ( ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> s C_ A )
282 simplll
 |-  ( ( ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> B C_ U. ran ( (,) o. f ) )
283 281 282 ssdif2d
 |-  ( ( ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( s \ U. ran ( (,) o. f ) ) C_ ( A \ B ) )
284 fveq2
 |-  ( ( s \ U. ran ( (,) o. f ) ) = b -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) )
285 284 eqcoms
 |-  ( b = ( s \ U. ran ( (,) o. f ) ) -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) )
286 285 biantrud
 |-  ( b = ( s \ U. ran ( (,) o. f ) ) -> ( b C_ ( A \ B ) <-> ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) ) )
287 sseq1
 |-  ( b = ( s \ U. ran ( (,) o. f ) ) -> ( b C_ ( A \ B ) <-> ( s \ U. ran ( (,) o. f ) ) C_ ( A \ B ) ) )
288 286 287 bitr3d
 |-  ( b = ( s \ U. ran ( (,) o. f ) ) -> ( ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) <-> ( s \ U. ran ( (,) o. f ) ) C_ ( A \ B ) ) )
289 288 rspcev
 |-  ( ( ( s \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s \ U. ran ( (,) o. f ) ) C_ ( A \ B ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) )
290 280 283 289 syl2anc
 |-  ( ( ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) )
291 290 adantlll
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) )
292 difss
 |-  ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) C_ ( A \ B )
293 292 3 sstri
 |-  ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) C_ A
294 ovolsscl
 |-  ( ( ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) e. RR )
295 293 294 mp3an1
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) e. RR )
296 295 ad5antr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) e. RR )
297 5 ad5antr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( A \ B ) ) e. RR )
298 simpl
 |-  ( ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) -> u e. RR )
299 298 ad4antlr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> u e. RR )
300 difdif2
 |-  ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) = ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) )
301 300 fveq2i
 |-  ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) = ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) )
302 difss
 |-  ( ( A \ B ) \ s ) C_ ( A \ B )
303 302 3 sstri
 |-  ( ( A \ B ) \ s ) C_ A
304 inss1
 |-  ( ( A \ B ) i^i U. ran ( (,) o. f ) ) C_ ( A \ B )
305 304 3 sstri
 |-  ( ( A \ B ) i^i U. ran ( (,) o. f ) ) C_ A
306 303 305 unssi
 |-  ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) C_ A
307 ovolsscl
 |-  ( ( ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) e. RR )
308 306 307 mp3an1
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) e. RR )
309 308 ad5antr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) e. RR )
310 difss
 |-  ( A \ s ) C_ A
311 ovolsscl
 |-  ( ( ( A \ s ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ s ) ) e. RR )
312 310 311 mp3an1
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ s ) ) e. RR )
313 312 ad5antr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( A \ s ) ) e. RR )
314 169 194 readdcld
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR )
315 314 250 jctil
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) e. RR* /\ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) )
316 simpr
 |-  ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) )
317 ovolge0
 |-  ( U. ran ( (,) o. f ) C_ RR -> 0 <_ ( vol* ` U. ran ( (,) o. f ) ) )
318 248 317 ax-mp
 |-  0 <_ ( vol* ` U. ran ( (,) o. f ) )
319 316 318 jctil
 |-  ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> ( 0 <_ ( vol* ` U. ran ( (,) o. f ) ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
320 xrrege0
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR* /\ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) /\ ( 0 <_ ( vol* ` U. ran ( (,) o. f ) ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. RR )
321 315 319 320 syl2an
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. RR )
322 difss
 |-  ( U. ran ( (,) o. f ) \ w ) C_ U. ran ( (,) o. f )
323 ovolsscl
 |-  ( ( ( U. ran ( (,) o. f ) \ w ) C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR )
324 322 248 323 mp3an12
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR )
325 321 324 syl
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR )
326 325 ad2antrr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR )
327 313 326 readdcld
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) e. RR )
328 5 50 sylan
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ u e. RR ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR )
329 328 adantrr
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR )
330 329 adantlr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR )
331 330 ad3antrrr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR )
332 ssdifss
 |-  ( A C_ RR -> ( A \ s ) C_ RR )
333 322 248 sstri
 |-  ( U. ran ( (,) o. f ) \ w ) C_ RR
334 unss
 |-  ( ( ( A \ s ) C_ RR /\ ( U. ran ( (,) o. f ) \ w ) C_ RR ) <-> ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) C_ RR )
335 332 333 334 sylanblc
 |-  ( A C_ RR -> ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) C_ RR )
336 ovolcl
 |-  ( ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) C_ RR -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR* )
337 335 336 syl
 |-  ( A C_ RR -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR* )
338 337 ad4antr
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR* )
339 312 ad3antrrr
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( A \ s ) ) e. RR )
340 339 325 readdcld
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) e. RR )
341 ovolge0
 |-  ( ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) C_ RR -> 0 <_ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) )
342 335 341 syl
 |-  ( A C_ RR -> 0 <_ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) )
343 342 ad4antr
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> 0 <_ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) )
344 332 adantr
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( A \ s ) C_ RR )
345 344 312 jca
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( ( A \ s ) C_ RR /\ ( vol* ` ( A \ s ) ) e. RR ) )
346 345 ad3antrrr
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( A \ s ) C_ RR /\ ( vol* ` ( A \ s ) ) e. RR ) )
347 325 333 jctil
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( U. ran ( (,) o. f ) \ w ) C_ RR /\ ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR ) )
348 ovolun
 |-  ( ( ( ( A \ s ) C_ RR /\ ( vol* ` ( A \ s ) ) e. RR ) /\ ( ( U. ran ( (,) o. f ) \ w ) C_ RR /\ ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) )
349 346 347 348 syl2anc
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) )
350 xrrege0
 |-  ( ( ( ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR* /\ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) e. RR ) /\ ( 0 <_ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) /\ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR )
351 338 340 343 349 350 syl22anc
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR )
352 351 ad2antrr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR )
353 ssdif
 |-  ( ( A \ B ) C_ A -> ( ( A \ B ) \ s ) C_ ( A \ s ) )
354 3 353 ax-mp
 |-  ( ( A \ B ) \ s ) C_ ( A \ s )
355 incom
 |-  ( ( A \ B ) i^i U. ran ( (,) o. f ) ) = ( U. ran ( (,) o. f ) i^i ( A \ B ) )
356 indif2
 |-  ( U. ran ( (,) o. f ) i^i ( A \ B ) ) = ( ( U. ran ( (,) o. f ) i^i A ) \ B )
357 355 356 eqtri
 |-  ( ( A \ B ) i^i U. ran ( (,) o. f ) ) = ( ( U. ran ( (,) o. f ) i^i A ) \ B )
358 inss1
 |-  ( U. ran ( (,) o. f ) i^i A ) C_ U. ran ( (,) o. f )
359 358 a1i
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( U. ran ( (,) o. f ) i^i A ) C_ U. ran ( (,) o. f ) )
360 simprrl
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> w C_ B )
361 359 360 ssdif2d
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( U. ran ( (,) o. f ) i^i A ) \ B ) C_ ( U. ran ( (,) o. f ) \ w ) )
362 357 361 eqsstrid
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( A \ B ) i^i U. ran ( (,) o. f ) ) C_ ( U. ran ( (,) o. f ) \ w ) )
363 unss12
 |-  ( ( ( ( A \ B ) \ s ) C_ ( A \ s ) /\ ( ( A \ B ) i^i U. ran ( (,) o. f ) ) C_ ( U. ran ( (,) o. f ) \ w ) ) -> ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) C_ ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) )
364 354 362 363 sylancr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) C_ ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) )
365 335 ad6antr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) C_ RR )
366 ovolss
 |-  ( ( ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) C_ ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) /\ ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) C_ RR ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) <_ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) )
367 364 365 366 syl2anc
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) <_ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) )
368 332 ad6antr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( A \ s ) C_ RR )
369 326 333 jctil
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( U. ran ( (,) o. f ) \ w ) C_ RR /\ ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR ) )
370 368 313 369 348 syl21anc
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) )
371 309 352 327 367 370 letrd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) )
372 194 ad3antrrr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR )
373 194 194 readdcld
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR )
374 373 ad3antrrr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR )
375 eleq1w
 |-  ( b = s -> ( b e. dom vol <-> s e. dom vol ) )
376 375 34 vtoclga
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> s e. dom vol )
377 mblvol
 |-  ( s e. dom vol -> ( vol ` s ) = ( vol* ` s ) )
378 376 377 syl
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol ` s ) = ( vol* ` s ) )
379 378 adantr
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( vol ` s ) = ( vol* ` s ) )
380 sseqin2
 |-  ( s C_ A <-> ( A i^i s ) = s )
381 380 biimpi
 |-  ( s C_ A -> ( A i^i s ) = s )
382 381 eqcomd
 |-  ( s C_ A -> s = ( A i^i s ) )
383 382 fveq2d
 |-  ( s C_ A -> ( vol* ` s ) = ( vol* ` ( A i^i s ) ) )
384 383 ad2antrr
 |-  ( ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) -> ( vol* ` s ) = ( vol* ` ( A i^i s ) ) )
385 379 384 sylan9eq
 |-  ( ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` s ) = ( vol* ` ( A i^i s ) ) )
386 385 oveq2d
 |-  ( ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` A ) - ( vol ` s ) ) = ( ( vol* ` A ) - ( vol* ` ( A i^i s ) ) ) )
387 386 adantll
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` A ) - ( vol ` s ) ) = ( ( vol* ` A ) - ( vol* ` ( A i^i s ) ) ) )
388 376 adantr
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> s e. dom vol )
389 simplll
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
390 mblsplit
 |-  ( ( s e. dom vol /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` A ) = ( ( vol* ` ( A i^i s ) ) + ( vol* ` ( A \ s ) ) ) )
391 390 eqcomd
 |-  ( ( s e. dom vol /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( ( vol* ` ( A i^i s ) ) + ( vol* ` ( A \ s ) ) ) = ( vol* ` A ) )
392 391 3expb
 |-  ( ( s e. dom vol /\ ( A C_ RR /\ ( vol* ` A ) e. RR ) ) -> ( ( vol* ` ( A i^i s ) ) + ( vol* ` ( A \ s ) ) ) = ( vol* ` A ) )
393 388 389 392 syl2anr
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> ( ( vol* ` ( A i^i s ) ) + ( vol* ` ( A \ s ) ) ) = ( vol* ` A ) )
394 393 adantr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( A i^i s ) ) + ( vol* ` ( A \ s ) ) ) = ( vol* ` A ) )
395 simp-6r
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` A ) e. RR )
396 395 recnd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` A ) e. CC )
397 inss1
 |-  ( A i^i s ) C_ A
398 ovolsscl
 |-  ( ( ( A i^i s ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A i^i s ) ) e. RR )
399 397 398 mp3an1
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A i^i s ) ) e. RR )
400 399 recnd
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A i^i s ) ) e. CC )
401 400 ad5antr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( A i^i s ) ) e. CC )
402 312 recnd
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ s ) ) e. CC )
403 402 ad5antr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( A \ s ) ) e. CC )
404 396 401 403 subaddd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` A ) - ( vol* ` ( A i^i s ) ) ) = ( vol* ` ( A \ s ) ) <-> ( ( vol* ` ( A i^i s ) ) + ( vol* ` ( A \ s ) ) ) = ( vol* ` A ) ) )
405 394 404 mpbird
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` A ) - ( vol* ` ( A i^i s ) ) ) = ( vol* ` ( A \ s ) ) )
406 387 405 eqtrd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` A ) - ( vol ` s ) ) = ( vol* ` ( A \ s ) ) )
407 379 ad2antlr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` s ) = ( vol* ` s ) )
408 simpll
 |-  ( ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) -> s C_ A )
409 simp-4l
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
410 ovolsscl
 |-  ( ( s C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` s ) e. RR )
411 410 3expb
 |-  ( ( s C_ A /\ ( A C_ RR /\ ( vol* ` A ) e. RR ) ) -> ( vol* ` s ) e. RR )
412 408 409 411 syl2anr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` s ) e. RR )
413 407 412 eqeltrd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` s ) e. RR )
414 simprlr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) )
415 395 372 413 414 ltsub23d
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` A ) - ( vol ` s ) ) < ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) )
416 406 415 eqbrtrrd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( A \ s ) ) < ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) )
417 321 recnd
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. CC )
418 417 ad2antrr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. CC )
419 240 ad5antlr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` B ) e. RR )
420 419 recnd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` B ) e. CC )
421 eleq1w
 |-  ( b = w -> ( b e. dom vol <-> w e. dom vol ) )
422 421 34 vtoclga
 |-  ( w e. ( Clsd ` ( topGen ` ran (,) ) ) -> w e. dom vol )
423 mblvol
 |-  ( w e. dom vol -> ( vol ` w ) = ( vol* ` w ) )
424 422 423 syl
 |-  ( w e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol ` w ) = ( vol* ` w ) )
425 424 adantl
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( vol ` w ) = ( vol* ` w ) )
426 425 ad2antlr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` w ) = ( vol* ` w ) )
427 simprl
 |-  ( ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) -> w C_ B )
428 simp-4r
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> ( B C_ RR /\ ( vol* ` B ) e. RR ) )
429 ovolsscl
 |-  ( ( w C_ B /\ B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` w ) e. RR )
430 429 3expb
 |-  ( ( w C_ B /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` w ) e. RR )
431 427 428 430 syl2anr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` w ) e. RR )
432 426 431 eqeltrd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` w ) e. RR )
433 432 recnd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` w ) e. CC )
434 418 420 433 npncand
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) + ( ( vol* ` B ) - ( vol ` w ) ) ) = ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol ` w ) ) )
435 simplrl
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> B C_ U. ran ( (,) o. f ) )
436 427 435 sylan9ssr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> w C_ U. ran ( (,) o. f ) )
437 sseqin2
 |-  ( w C_ U. ran ( (,) o. f ) <-> ( U. ran ( (,) o. f ) i^i w ) = w )
438 436 437 sylib
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( U. ran ( (,) o. f ) i^i w ) = w )
439 438 fveq2d
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) = ( vol* ` w ) )
440 426 439 eqtr4d
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` w ) = ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) )
441 440 oveq2d
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol ` w ) ) = ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) ) )
442 422 adantl
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> w e. dom vol )
443 321 248 jctil
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) )
444 mblsplit
 |-  ( ( w e. dom vol /\ U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` U. ran ( (,) o. f ) ) = ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) )
445 444 eqcomd
 |-  ( ( w e. dom vol /\ U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) )
446 445 3expb
 |-  ( ( w e. dom vol /\ ( U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) ) -> ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) )
447 442 443 446 syl2anr
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) )
448 447 adantr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) )
449 inss1
 |-  ( U. ran ( (,) o. f ) i^i w ) C_ U. ran ( (,) o. f )
450 ovolsscl
 |-  ( ( ( U. ran ( (,) o. f ) i^i w ) C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) e. RR )
451 449 248 450 mp3an12
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) e. RR )
452 321 451 syl
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) e. RR )
453 452 recnd
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) e. CC )
454 325 recnd
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. CC )
455 417 453 454 subaddd
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) ) = ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) <-> ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) ) )
456 455 ad2antrr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) ) = ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) <-> ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) ) )
457 448 456 mpbird
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) ) = ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) )
458 434 441 457 3eqtrd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) + ( ( vol* ` B ) - ( vol ` w ) ) ) = ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) )
459 240 ad3antlr
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` B ) e. RR )
460 321 459 resubcld
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) e. RR )
461 460 ad2antrr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) e. RR )
462 419 432 resubcld
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` B ) - ( vol ` w ) ) e. RR )
463 simprr
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) )
464 194 adantr
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR )
465 321 459 464 lesubadd2d
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) <_ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) <-> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
466 463 465 mpbird
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) <_ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) )
467 466 ad2antrr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) <_ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) )
468 simprrr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) )
469 419 372 432 468 ltsub23d
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` B ) - ( vol ` w ) ) < ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) )
470 461 462 372 372 467 469 leltaddd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) + ( ( vol* ` B ) - ( vol ` w ) ) ) < ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) )
471 458 470 eqbrtrrd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) < ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) )
472 313 326 372 374 416 471 lt2addd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) < ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
473 df-3
 |-  3 = ( 2 + 1 )
474 2cn
 |-  2 e. CC
475 ax-1cn
 |-  1 e. CC
476 474 475 addcomi
 |-  ( 2 + 1 ) = ( 1 + 2 )
477 473 476 eqtri
 |-  3 = ( 1 + 2 )
478 477 oveq1i
 |-  ( 3 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( 1 + 2 ) x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) )
479 62 rpcnd
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. CC )
480 adddir
 |-  ( ( 1 e. CC /\ 2 e. CC /\ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. CC ) -> ( ( 1 + 2 ) x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( 1 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) + ( 2 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
481 475 474 480 mp3an12
 |-  ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. CC -> ( ( 1 + 2 ) x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( 1 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) + ( 2 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
482 479 481 syl
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( 1 + 2 ) x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( 1 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) + ( 2 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
483 479 mulid2d
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( 1 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) )
484 479 2timesd
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( 2 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) )
485 483 484 oveq12d
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( 1 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) + ( 2 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) = ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
486 482 485 eqtrd
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( 1 + 2 ) x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
487 478 486 syl5eq
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( 3 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) )
488 329 recnd
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - u ) e. CC )
489 3cn
 |-  3 e. CC
490 3ne0
 |-  3 =/= 0
491 divcan2
 |-  ( ( ( ( vol* ` ( A \ B ) ) - u ) e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( 3 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( vol* ` ( A \ B ) ) - u ) )
492 489 490 491 mp3an23
 |-  ( ( ( vol* ` ( A \ B ) ) - u ) e. CC -> ( 3 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( vol* ` ( A \ B ) ) - u ) )
493 488 492 syl
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( 3 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( vol* ` ( A \ B ) ) - u ) )
494 487 493 eqtr3d
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) = ( ( vol* ` ( A \ B ) ) - u ) )
495 494 adantlr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) = ( ( vol* ` ( A \ B ) ) - u ) )
496 495 ad3antrrr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) = ( ( vol* ` ( A \ B ) ) - u ) )
497 472 496 breqtrd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) < ( ( vol* ` ( A \ B ) ) - u ) )
498 309 327 331 371 497 lelttrd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) < ( ( vol* ` ( A \ B ) ) - u ) )
499 301 498 eqbrtrid
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) < ( ( vol* ` ( A \ B ) ) - u ) )
500 296 297 299 499 ltsub13d
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> u < ( ( vol* ` ( A \ B ) ) - ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) )
501 283 adantlll
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( s \ U. ran ( (,) o. f ) ) C_ ( A \ B ) )
502 sseqin2
 |-  ( ( s \ U. ran ( (,) o. f ) ) C_ ( A \ B ) <-> ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) = ( s \ U. ran ( (,) o. f ) ) )
503 501 502 sylib
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) = ( s \ U. ran ( (,) o. f ) ) )
504 503 fveq2d
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. f ) ) ) )
505 opnmbl
 |-  ( U. ran ( (,) o. f ) e. ( topGen ` ran (,) ) -> U. ran ( (,) o. f ) e. dom vol )
506 273 505 ax-mp
 |-  U. ran ( (,) o. f ) e. dom vol
507 difmbl
 |-  ( ( s e. dom vol /\ U. ran ( (,) o. f ) e. dom vol ) -> ( s \ U. ran ( (,) o. f ) ) e. dom vol )
508 376 506 507 sylancl
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s \ U. ran ( (,) o. f ) ) e. dom vol )
509 508 adantr
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( s \ U. ran ( (,) o. f ) ) e. dom vol )
510 509 ad2antlr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( s \ U. ran ( (,) o. f ) ) e. dom vol )
511 13 adantr
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( A \ B ) C_ RR )
512 511 5 jca
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( ( A \ B ) C_ RR /\ ( vol* ` ( A \ B ) ) e. RR ) )
513 512 ad5antr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( A \ B ) C_ RR /\ ( vol* ` ( A \ B ) ) e. RR ) )
514 mblsplit
 |-  ( ( ( s \ U. ran ( (,) o. f ) ) e. dom vol /\ ( A \ B ) C_ RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( vol* ` ( A \ B ) ) = ( ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) + ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) )
515 514 3expb
 |-  ( ( ( s \ U. ran ( (,) o. f ) ) e. dom vol /\ ( ( A \ B ) C_ RR /\ ( vol* ` ( A \ B ) ) e. RR ) ) -> ( vol* ` ( A \ B ) ) = ( ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) + ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) )
516 515 eqcomd
 |-  ( ( ( s \ U. ran ( (,) o. f ) ) e. dom vol /\ ( ( A \ B ) C_ RR /\ ( vol* ` ( A \ B ) ) e. RR ) ) -> ( ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) + ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) = ( vol* ` ( A \ B ) ) )
517 510 513 516 syl2anc
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) + ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) = ( vol* ` ( A \ B ) ) )
518 297 recnd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( A \ B ) ) e. CC )
519 296 recnd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) e. CC )
520 inss1
 |-  ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) C_ ( A \ B )
521 520 3 sstri
 |-  ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) C_ A
522 ovolsscl
 |-  ( ( ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) e. RR )
523 521 522 mp3an1
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) e. RR )
524 523 ad5antr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) e. RR )
525 524 recnd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) e. CC )
526 518 519 525 subadd2d
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) = ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) <-> ( ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) + ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) = ( vol* ` ( A \ B ) ) ) )
527 517 526 mpbird
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) = ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) )
528 mblvol
 |-  ( ( s \ U. ran ( (,) o. f ) ) e. dom vol -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. f ) ) ) )
529 507 528 syl
 |-  ( ( s e. dom vol /\ U. ran ( (,) o. f ) e. dom vol ) -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. f ) ) ) )
530 376 506 529 sylancl
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. f ) ) ) )
531 530 adantr
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. f ) ) ) )
532 531 ad2antlr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. f ) ) ) )
533 504 527 532 3eqtr4rd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( ( vol* ` ( A \ B ) ) - ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) )
534 500 533 breqtrrd
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> u < ( vol ` ( s \ U. ran ( (,) o. f ) ) ) )
535 fvex
 |-  ( vol ` ( s \ U. ran ( (,) o. f ) ) ) e. _V
536 eqeq1
 |-  ( v = ( vol ` ( s \ U. ran ( (,) o. f ) ) ) -> ( v = ( vol ` b ) <-> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) )
537 536 anbi2d
 |-  ( v = ( vol ` ( s \ U. ran ( (,) o. f ) ) ) -> ( ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) <-> ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) ) )
538 537 rexbidv
 |-  ( v = ( vol ` ( s \ U. ran ( (,) o. f ) ) ) -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) ) )
539 breq2
 |-  ( v = ( vol ` ( s \ U. ran ( (,) o. f ) ) ) -> ( u < v <-> u < ( vol ` ( s \ U. ran ( (,) o. f ) ) ) ) )
540 538 539 anbi12d
 |-  ( v = ( vol ` ( s \ U. ran ( (,) o. f ) ) ) -> ( ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) /\ u < v ) <-> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) /\ u < ( vol ` ( s \ U. ran ( (,) o. f ) ) ) ) ) )
541 535 540 spcev
 |-  ( ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) /\ u < ( vol ` ( s \ U. ran ( (,) o. f ) ) ) ) -> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) /\ u < v ) )
542 291 534 541 syl2anc
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) /\ u < v ) )
543 148 anbi2d
 |-  ( y = v -> ( ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) <-> ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) ) )
544 543 rexbidv
 |-  ( y = v -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) ) )
545 544 rexab
 |-  ( E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v <-> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) /\ u < v ) )
546 542 545 sylibr
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v )
547 546 ex
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> ( ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) )
548 547 rexlimdvva
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( E. s e. ( Clsd ` ( topGen ` ran (,) ) ) E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) )
549 260 548 exlimddv
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( E. s e. ( Clsd ` ( topGen ` ran (,) ) ) E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) )
550 221 549 syld
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) )
551 550 exp31
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) -> ( ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) ) ) )
552 551 com34
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) ) ) )
553 552 3imp1
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v )
554 2 6 48 553 eqsupd
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) ) -> sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } , RR , < ) = ( vol* ` ( A \ B ) ) )