Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mblfinlem2 Unicode version

Theorem mblfinlem2 26144
Description: The difference between two sets measurable by the criterion in ismblfin 26146 is itself measurable by the same. Proposition 0.3 of [Viaclovsky7] p. 3. (Contributed by Brendan Leahy, 25-Mar-2018.)
Assertion
Ref Expression
mblfinlem2  |-  ( ( ( 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 ) ) )
Distinct variable groups:    y, b, A    B, b, y

Proof of Theorem mblfinlem2
Dummy variables  f 
s  u  v  w  x  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltso 9112 . . 3  |-  <  Or  RR
21a1i 11 . 2  |-  ( ( ( 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 3434 . . . 4  |-  ( A 
\  B )  C_  A
4 ovolsscl 19335 . . . 4  |-  ( ( ( A  \  B
)  C_  A  /\  A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( vol * `  ( A  \  B ) )  e.  RR )
53, 4mp3an1 1266 . . 3  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( vol * `  ( A  \  B ) )  e.  RR )
653ad2ant1 978 . 2  |-  ( ( ( 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 2919 . . . . . 6  |-  u  e. 
_V
8 eqeq1 2410 . . . . . . . 8  |-  ( y  =  u  ->  (
y  =  ( vol `  b )  <->  u  =  ( vol `  b ) ) )
98anbi2d 685 . . . . . . 7  |-  ( y  =  u  ->  (
( b  C_  ( A  \  B )  /\  y  =  ( vol `  b ) )  <->  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) ) )
109rexbidv 2687 . . . . . 6  |-  ( 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 ) ) ) )
117, 10elab 3042 . . . . 5  |-  ( 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 733 . . . . . . . . 9  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) )  ->  b  C_  ( A  \  B
) )
13 ssdifss 3438 . . . . . . . . 9  |-  ( A 
C_  RR  ->  ( A 
\  B )  C_  RR )
14 ovolss 19334 . . . . . . . . 9  |-  ( ( b  C_  ( A  \  B )  /\  ( A  \  B )  C_  RR )  ->  ( vol
* `  b )  <_  ( vol * `  ( A  \  B ) ) )
1512, 13, 14syl2anr 465 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) ) )  -> 
( vol * `  b )  <_  ( vol * `  ( A 
\  B ) ) )
16 uniretop 18749 . . . . . . . . . . . . 13  |-  RR  =  U. ( topGen `  ran  (,) )
1716cldss 17048 . . . . . . . . . . . 12  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  C_  RR )
18 ovolcl 19327 . . . . . . . . . . . 12  |-  ( b 
C_  RR  ->  ( vol
* `  b )  e.  RR* )
1917, 18syl 16 . . . . . . . . . . 11  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol * `
 b )  e. 
RR* )
20 ovolcl 19327 . . . . . . . . . . . 12  |-  ( ( A  \  B ) 
C_  RR  ->  ( vol
* `  ( A  \  B ) )  e. 
RR* )
2113, 20syl 16 . . . . . . . . . . 11  |-  ( A 
C_  RR  ->  ( vol
* `  ( A  \  B ) )  e. 
RR* )
22 xrlenlt 9099 . . . . . . . . . . 11  |-  ( ( ( vol * `  b )  e.  RR*  /\  ( vol * `  ( A  \  B ) )  e.  RR* )  ->  ( ( vol * `  b )  <_  ( vol * `  ( A 
\  B ) )  <->  -.  ( vol * `  ( A  \  B ) )  <  ( vol
* `  b )
) )
2319, 21, 22syl2anr 465 . . . . . . . . . 10  |-  ( ( A  C_  RR  /\  b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )  ->  (
( vol * `  b )  <_  ( vol * `  ( A 
\  B ) )  <->  -.  ( vol * `  ( A  \  B ) )  <  ( vol
* `  b )
) )
2423adantrr 698 . . . . . . . . 9  |-  ( ( 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 20 . . . . . . . . . . . . . 14  |-  ( u  =  ( vol `  b
)  ->  u  =  ( vol `  b ) )
26 dfss4 3535 . . . . . . . . . . . . . . . . 17  |-  ( b 
C_  RR  <->  ( RR  \ 
( RR  \  b
) )  =  b )
2717, 26sylib 189 . . . . . . . . . . . . . . . 16  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  =  b )
28 rembl 19388 . . . . . . . . . . . . . . . . 17  |-  RR  e.  dom  vol
2916cldopn 17050 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  (
topGen `  ran  (,) )
)
30 opnmbl 19447 . . . . . . . . . . . . . . . . . 18  |-  ( ( RR  \  b )  e.  ( topGen `  ran  (,) )  ->  ( RR  \  b )  e.  dom  vol )
3129, 30syl 16 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  dom  vol )
32 difmbl 19390 . . . . . . . . . . . . . . . . 17  |-  ( ( RR  e.  dom  vol  /\  ( RR  \  b
)  e.  dom  vol )  ->  ( RR  \ 
( RR  \  b
) )  e.  dom  vol )
3328, 31, 32sylancr 645 . . . . . . . . . . . . . . . 16  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  e.  dom  vol )
3427, 33eqeltrrd 2479 . . . . . . . . . . . . . . 15  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  e.  dom  vol )
35 mblvol 19379 . . . . . . . . . . . . . . 15  |-  ( b  e.  dom  vol  ->  ( vol `  b )  =  ( vol * `  b ) )
3634, 35syl 16 . . . . . . . . . . . . . 14  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  b )  =  ( vol * `  b
) )
3725, 36sylan9eqr 2458 . . . . . . . . . . . . 13  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  u  =  ( vol `  b ) )  ->  u  =  ( vol * `  b
) )
3837breq2d 4184 . . . . . . . . . . . 12  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  u  =  ( vol `  b ) )  ->  ( ( vol * `  ( A 
\  B ) )  <  u  <->  ( vol * `
 ( A  \  B ) )  < 
( vol * `  b ) ) )
3938notbid 286 . . . . . . . . . . 11  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  u  =  ( vol `  b ) )  ->  ( -.  ( vol * `  ( A  \  B ) )  <  u  <->  -.  ( vol * `  ( A 
\  B ) )  <  ( vol * `  b ) ) )
4039adantrl 697 . . . . . . . . . 10  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) )  ->  ( -.  ( vol * `  ( A  \  B ) )  <  u  <->  -.  ( vol * `  ( A 
\  B ) )  <  ( vol * `  b ) ) )
4140adantl 453 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) ) )  -> 
( -.  ( vol
* `  ( A  \  B ) )  < 
u  <->  -.  ( vol * `
 ( A  \  B ) )  < 
( vol * `  b ) ) )
4224, 41bitr4d 248 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) ) )  -> 
( ( vol * `  b )  <_  ( vol * `  ( A 
\  B ) )  <->  -.  ( vol * `  ( A  \  B ) )  <  u ) )
4315, 42mpbid 202 . . . . . . 7  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) ) )  ->  -.  ( vol * `  ( A  \  B ) )  <  u )
4443rexlimdvaa 2791 . . . . . 6  |-  ( A 
C_  RR  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  ( A  \  B )  /\  u  =  ( vol `  b ) )  ->  -.  ( vol * `  ( A 
\  B ) )  <  u ) )
4544imp 419 . . . . 5  |-  ( ( A  C_  RR  /\  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  ( A  \  B )  /\  u  =  ( vol `  b ) ) )  ->  -.  ( vol * `  ( A  \  B ) )  <  u )
4611, 45sylan2b 462 . . . 4  |-  ( ( A  C_  RR  /\  u  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  ( A  \  B )  /\  y  =  ( vol `  b ) ) } )  ->  -.  ( vol * `  ( A  \  B ) )  <  u )
4746adantlr 696 . . 3  |-  ( ( ( 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 )
48473ad2antl1 1119 . 2  |-  ( ( ( ( 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 732 . . . . . . . . . . . . . . 15  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( vol * `  A )  e.  RR )
50 resubcl 9321 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  u  e.  RR )  ->  ( ( vol * `  ( A  \  B
) )  -  u
)  e.  RR )
5150adantrr 698 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  ( A  \  B ) ) ) )  ->  ( ( vol * `  ( A 
\  B ) )  -  u )  e.  RR )
52 posdif 9477 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( u  e.  RR  /\  ( vol * `  ( A  \  B ) )  e.  RR )  -> 
( u  <  ( vol * `  ( A 
\  B ) )  <->  0  <  ( ( vol * `  ( A  \  B ) )  -  u ) ) )
5352ancoms 440 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  u  e.  RR )  ->  ( u  <  ( vol * `  ( A 
\  B ) )  <->  0  <  ( ( vol * `  ( A  \  B ) )  -  u ) ) )
5453biimpd 199 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  u  e.  RR )  ->  ( u  <  ( vol * `  ( A 
\  B ) )  ->  0  <  (
( vol * `  ( A  \  B ) )  -  u ) ) )
5554impr 603 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  ( A  \  B ) ) ) )  ->  0  <  ( ( vol * `  ( A  \  B ) )  -  u ) )
5651, 55elrpd 10602 . . . . . . . . . . . . . . . . 17  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  ( A  \  B ) ) ) )  ->  ( ( vol * `  ( A 
\  B ) )  -  u )  e.  RR+ )
57 3nn 10090 . . . . . . . . . . . . . . . . . 18  |-  3  e.  NN
58 nnrp 10577 . . . . . . . . . . . . . . . . . 18  |-  ( 3  e.  NN  ->  3  e.  RR+ )
5957, 58ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  3  e.  RR+
60 rpdivcl 10590 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( vol * `  ( A  \  B
) )  -  u
)  e.  RR+  /\  3  e.  RR+ )  ->  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 )  e.  RR+ )
6156, 59, 60sylancl 644 . . . . . . . . . . . . . . . 16  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  ( A  \  B ) ) ) )  ->  ( (
( vol * `  ( A  \  B ) )  -  u )  /  3 )  e.  RR+ )
625, 61sylan 458 . . . . . . . . . . . . . . 15  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( ( ( vol
* `  ( A  \  B ) )  -  u )  /  3
)  e.  RR+ )
6349, 62ltsubrpd 10632 . . . . . . . . . . . . . 14  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( ( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol
* `  A )
)
6463adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 448 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ,  <  ) )
6664, 65breqtrd 4196 . . . . . . . . . . . 12  |-  ( ( ( ( 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 9037 . . . . . . . . . . . . . . . . . 18  |-  RR  e.  _V
6867ssex 4307 . . . . . . . . . . . . . . . . 17  |-  ( A 
C_  RR  ->  A  e. 
_V )
6968adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  ->  A  e.  _V )
70 sseq1 3329 . . . . . . . . . . . . . . . . . . 19  |-  ( v  =  A  ->  (
v  C_  RR  <->  A  C_  RR ) )
71 fveq2 5687 . . . . . . . . . . . . . . . . . . . 20  |-  ( v  =  A  ->  ( vol * `  v )  =  ( vol * `  A ) )
7271eleq1d 2470 . . . . . . . . . . . . . . . . . . 19  |-  ( v  =  A  ->  (
( vol * `  v )  e.  RR  <->  ( vol * `  A
)  e.  RR ) )
7370, 72anbi12d 692 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  A  ->  (
( v  C_  RR  /\  ( vol * `  v )  e.  RR ) 
<->  ( A  C_  RR  /\  ( vol * `  A )  e.  RR ) ) )
74 sseq2 3330 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  =  A  ->  (
b  C_  v  <->  b  C_  A ) )
7574anbi1d 686 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  =  A  ->  (
( b  C_  v  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  y  =  ( vol `  b ) ) ) )
7675rexbidv 2687 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) ) )
7776abbidv 2518 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) } )
7877sseq1d 3335 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) )
7977neeq1d 2580 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) }  =/=  (/) ) )
8077raleqdv 2870 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) )
8180rexbidv 2687 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) )
8278, 79, 813anbi123d 1254 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) )
8373, 82imbi12d 312 . . . . . . . . . . . . . . . . 17  |-  ( 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 448 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b  C_  v  /\  y  =  ( vol `  b ) )  -> 
y  =  ( vol `  b ) )
8584, 36sylan9eqr 2458 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  y  =  ( vol `  b
) ) )  -> 
y  =  ( vol
* `  b )
)
8685adantl 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  /\  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( b  C_  v  /\  y  =  ( vol `  b
) ) ) )  ->  y  =  ( vol * `  b
) )
87 simprl 733 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  y  =  ( vol `  b
) ) )  -> 
b  C_  v )
88 ovolsscl 19335 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( b  C_  v  /\  v  C_  RR  /\  ( vol * `  v )  e.  RR )  -> 
( vol * `  b )  e.  RR )
89883expb 1154 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b  C_  v  /\  ( v  C_  RR  /\  ( vol * `  v )  e.  RR ) )  ->  ( vol * `  b )  e.  RR )
9089ancoms 440 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  /\  b  C_  v
)  ->  ( vol * `
 b )  e.  RR )
9187, 90sylan2 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  /\  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( b  C_  v  /\  y  =  ( vol `  b
) ) ) )  ->  ( vol * `  b )  e.  RR )
9286, 91eqeltrd 2478 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  /\  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( b  C_  v  /\  y  =  ( vol `  b
) ) ) )  ->  y  e.  RR )
9392rexlimdvaa 2791 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  -> 
( E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) )  ->  y  e.  RR ) )
9493abssdv 3377 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  ->  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  C_  RR )
95 retop 18748 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  Top
96 0cld 17057 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
topGen `  ran  (,) )  e.  Top  ->  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
9795, 96ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )
98 0ss 3616 . . . . . . . . . . . . . . . . . . . . . 22  |-  (/)  C_  v
99 0mbl 19387 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (/)  e.  dom  vol
100 mblvol 19379 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol * `  (/) ) )
10199, 100ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( vol `  (/) )  =  ( vol * `  (/) )
102 ovol0 19342 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( vol
* `  (/) )  =  0
103101, 102eqtr2i 2425 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  =  ( vol `  (/) )
10498, 103pm3.2i 442 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (/)  C_  v  /\  0  =  ( vol `  (/) ) )
105 sseq1 3329 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  =  (/)  ->  ( b 
C_  v  <->  (/)  C_  v
) )
106 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  =  (/)  ->  ( vol `  b )  =  ( vol `  (/) ) )
107106eqeq2d 2415 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  =  (/)  ->  ( 0  =  ( vol `  b
)  <->  0  =  ( vol `  (/) ) ) )
108105, 107anbi12d 692 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  (/)  ->  ( ( b  C_  v  /\  0  =  ( vol `  b ) )  <->  ( (/)  C_  v  /\  0  =  ( vol `  (/) ) ) ) )
109108rspcev 3012 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
(/)  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( (/)  C_  v  /\  0  =  ( vol `  (/) ) ) )  ->  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  v  /\  0  =  ( vol `  b ) ) )
11097, 104, 109mp2an 654 . . . . . . . . . . . . . . . . . . . 20  |-  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  0  =  ( vol `  b ) )
111 c0ex 9041 . . . . . . . . . . . . . . . . . . . . 21  |-  0  e.  _V
112 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  0  ->  (
y  =  ( vol `  b )  <->  0  =  ( vol `  b ) ) )
113112anbi2d 685 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  0  ->  (
( b  C_  v  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  v  /\  0  =  ( vol `  b ) ) ) )
114113rexbidv 2687 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) ) )
115111, 114spcev 3003 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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
) ) )
116110, 115ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  E. y E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  v  /\  y  =  ( vol `  b
) )
117 abn0 3606 . . . . . . . . . . . . . . . . . . . 20  |-  ( { 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
) ) )
118117biimpri 198 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) }  =/=  (/) )
119116, 118mp1i 12 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  ->  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =/=  (/) )
120 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( b  C_  v  /\  z  =  ( vol `  b ) )  -> 
z  =  ( vol `  b ) )
121120, 36sylan9eqr 2458 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  z  =  ( vol `  b
) ) )  -> 
z  =  ( vol
* `  b )
)
122121adantl 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  z  =  ( vol `  b
) ) ) )  ->  z  =  ( vol * `  b
) )
123 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  z  =  ( vol `  b
) ) )  -> 
b  C_  v )
124 ovolss 19334 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( b  C_  v  /\  v  C_  RR )  -> 
( vol * `  b )  <_  ( vol * `  v ) )
125124ancoms 440 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( v  C_  RR  /\  b  C_  v )  ->  ( vol * `  b )  <_  ( vol * `  v ) )
126123, 125sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  z  =  ( vol `  b
) ) ) )  ->  ( vol * `  b )  <_  ( vol * `  v ) )
127122, 126eqbrtrd 4192 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  z  =  ( vol `  b
) ) ) )  ->  z  <_  ( vol * `  v ) )
128127rexlimdvaa 2791 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v 
C_  RR  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  z  =  ( vol `  b ) )  ->  z  <_  ( vol * `  v
) ) )
129128alrimiv 1638 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v 
C_  RR  ->  A. z
( E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  z  =  ( vol `  b ) )  ->  z  <_  ( vol * `  v
) ) )
130 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  z  ->  (
y  =  ( vol `  b )  <->  z  =  ( vol `  b ) ) )
131130anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  z  ->  (
( b  C_  v  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  v  /\  z  =  ( vol `  b ) ) ) )
132131rexbidv 2687 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) ) )
133132ralab 3055 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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
) ) )
134129, 133sylibr 204 . . . . . . . . . . . . . . . . . . . 20  |-  ( v 
C_  RR  ->  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_ 
( vol * `  v ) )
135 breq2 4176 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( vol * `  v )  ->  (
z  <_  x  <->  z  <_  ( vol * `  v
) ) )
136135ralbidv 2686 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( vol * `  v )  ->  ( 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_  v  /\  y  =  ( vol `  b ) ) } z  <_ 
( vol * `  v ) ) )
137136rspcev 3012 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 )
138134, 137sylan2 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 )
139138ancoms 440 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 )
14094, 119, 1393jca 1134 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) )
14183, 140vtoclg 2971 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) )
14269, 141mpcom 34 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) )
143142adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) )
14462rpred 10604 . . . . . . . . . . . . . . 15  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( ( ( vol
* `  ( A  \  B ) )  -  u )  /  3
)  e.  RR )
14549, 144resubcld 9421 . . . . . . . . . . . . . 14  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( ( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  e.  RR )
146 suprlub 9926 . . . . . . . . . . . . . 14  |-  ( ( ( { 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 ) )
147143, 145, 146syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
148147adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
14966, 148mpbid 202 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
150 eqeq1 2410 . . . . . . . . . . . . . . 15  |-  ( y  =  v  ->  (
y  =  ( vol `  b )  <->  v  =  ( vol `  b ) ) )
151150anbi2d 685 . . . . . . . . . . . . . 14  |-  ( y  =  v  ->  (
( b  C_  A  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  v  =  ( vol `  b ) ) ) )
152151rexbidv 2687 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) )
153152rexab 3057 . . . . . . . . . . . 12  |-  ( 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 ) )
154 breq2 4176 . . . . . . . . . . . . . . . . 17  |-  ( v  =  ( vol `  b
)  ->  ( (
( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  v  <->  ( ( vol * `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  b
) ) )
155154ad2antll 710 . . . . . . . . . . . . . . . 16  |-  ( ( 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
) ) )
156 sseq1 3329 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  b  ->  (
s  C_  A  <->  b  C_  A ) )
157 fveq2 5687 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  b  ->  ( vol `  s )  =  ( vol `  b
) )
158157breq2d 4184 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  b  ->  (
( ( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  s )  <->  ( ( vol * `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  b
) ) )
159156, 158anbi12d 692 . . . . . . . . . . . . . . . . . . 19  |-  ( 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
) ) ) )
160159rspcev 3012 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) )
161160expr 599 . . . . . . . . . . . . . . . . 17  |-  ( ( 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
) ) ) )
162161adantrr 698 . . . . . . . . . . . . . . . 16  |-  ( ( 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
) ) ) )
163155, 162sylbid 207 . . . . . . . . . . . . . . 15  |-  ( ( 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
) ) ) )
164163rexlimiva 2785 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
165164imp 419 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) )
166165exlimiv 1641 . . . . . . . . . . . 12  |-  ( 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 ) ) )
167153, 166sylbi 188 . . . . . . . . . . 11  |-  ( 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
) ) )
168149, 167syl 16 . . . . . . . . . 10  |-  ( ( ( ( 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 ) ) )
169168ex 424 . . . . . . . . 9  |-  ( ( ( 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
) ) ) )
170169adantlr 696 . . . . . . . 8  |-  ( ( ( ( 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
) ) ) )
171 simplrr 738 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
17262adantlr 696 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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+ )
173171, 172ltsubrpd 10632 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) )
174173adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 )
)
175 simpr 448 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 ,  <  ) )
176174, 175breqtrd 4196 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 ,  <  ) )
17767ssex 4307 . . . . . . . . . . . . . . . 16  |-  ( B 
C_  RR  ->  B  e. 
_V )
178177adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( B  C_  RR  /\  ( vol * `  B )  e.  RR )  ->  B  e.  _V )
179 sseq1 3329 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  B  ->  (
v  C_  RR  <->  B  C_  RR ) )
180 fveq2 5687 . . . . . . . . . . . . . . . . . . 19  |-  ( v  =  B  ->  ( vol * `  v )  =  ( vol * `  B ) )
181180eleq1d 2470 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  B  ->  (
( vol * `  v )  e.  RR  <->  ( vol * `  B
)  e.  RR ) )
182179, 181anbi12d 692 . . . . . . . . . . . . . . . . 17  |-  ( v  =  B  ->  (
( v  C_  RR  /\  ( vol * `  v )  e.  RR ) 
<->  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) ) )
183 sseq2 3330 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  =  B  ->  (
b  C_  v  <->  b  C_  B ) )
184183anbi1d 686 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  =  B  ->  (
( b  C_  v  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  B  /\  y  =  ( vol `  b ) ) ) )
185184rexbidv 2687 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) ) )
186185abbidv 2518 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) } )
187186sseq1d 3335 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) )
188186neeq1d 2580 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) }  =/=  (/) ) )
189186raleqdv 2870 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) )
190189rexbidv 2687 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) )
191187, 188, 1903anbi123d 1254 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) )
192182, 191imbi12d 312 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) ) )
193192, 140vtoclg 2971 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) )
194178, 193mpcom 34 . . . . . . . . . . . . . 14  |-  ( ( 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 ) )
195194ad2antlr 708 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) )
196144adantlr 696 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
197171, 196resubcld 9421 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
198 suprlub 9926 . . . . . . . . . . . . 13  |-  ( ( ( { 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 ) )
199195, 197, 198syl2anc 643 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
200199adantr 452 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 ) )
201176, 200mpbid 202 . . . . . . . . . 10  |-  ( ( ( ( ( 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 )
202150anbi2d 685 . . . . . . . . . . . . 13  |-  ( y  =  v  ->  (
( b  C_  B  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  B  /\  v  =  ( vol `  b ) ) ) )
203202rexbidv 2687 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )
204203rexab 3057 . . . . . . . . . . 11  |-  ( 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 ) )
205 breq2 4176 . . . . . . . . . . . . . . . 16  |-  ( v  =  ( vol `  b
)  ->  ( (
( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  v  <->  ( ( vol * `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  b
) ) )
206205ad2antll 710 . . . . . . . . . . . . . . 15  |-  ( ( 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
) ) )
207 sseq1 3329 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  b  ->  (
w  C_  B  <->  b  C_  B ) )
208 fveq2 5687 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  b  ->  ( vol `  w )  =  ( vol `  b
) )
209208breq2d 4184 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  b  ->  (
( ( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  w )  <->  ( ( vol * `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  b
) ) )
210207, 209anbi12d 692 . . . . . . . . . . . . . . . . . 18  |-  ( 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
) ) ) )
211210rspcev 3012 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) ) )
212211expr 599 . . . . . . . . . . . . . . . 16  |-  ( ( 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
) ) ) )
213212adantrr 698 . . . . . . . . . . . . . . 15  |-  ( ( 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
) ) ) )
214206, 213sylbid 207 . . . . . . . . . . . . . 14  |-  ( ( 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
) ) ) )
215214rexlimiva 2785 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) )
216215imp 419 . . . . . . . . . . . 12  |-  ( ( 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 ) ) )
217216exlimiv 1641 . . . . . . . . . . 11  |-  ( 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 ) ) )
218204, 217sylbi 188 . . . . . . . . . 10  |-  ( 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
) ) )
219201, 218syl 16 . . . . . . . . 9  |-  ( ( ( ( ( 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 ) ) )
220219ex 424 . . . . . . . 8  |-  ( ( ( ( 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
) ) ) )
221170, 220anim12d 547 . . . . . . 7  |-  ( ( ( ( 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
) ) ) ) )
222 reeanv 2835 . . . . . . 7  |-  ( 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
) ) ) )
223221, 222syl6ibr 219 . . . . . 6  |-  ( ( ( ( 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 ) ) ) ) )
224 eqid 2404 . . . . . . . . . . . . . 14  |-  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
225224ovolgelb 19329 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) )
2262253expa 1153 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) )
22762, 226sylan2 461 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) )
228227ancoms 440 . . . . . . . . . 10  |-  ( ( ( ( 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 ) ) ) )
229228an32s 780 . . . . . . . . 9  |-  ( ( ( ( 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 )