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	imbitrrdi	|- ( ( ( ( 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		dfss2	|- ( 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	eqtrid	|- ( 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	mullidd	|- ( ( ( 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	eqtrid	|- ( ( ( 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 ) ) )