let I be non empty closed_interval Subset of REAL; :: thesis: for jauge1, jauge2 being positive-yielding Function of I,REAL
for TD being b₁ -fine tagged_division of I st jauge1 <= jauge2 holds
TD is b₂ -fine tagged_division of I
let jauge1, jauge2 be positive-yielding Function of I,REAL; :: thesis: for TD being jauge1 -fine tagged_division of I st jauge1 <= jauge2 holds
TD is jauge2 -fine tagged_division of I
let TD be jauge1 -fine tagged_division of I; :: thesis: ( jauge1 <= jauge2 implies TD is jauge2 -fine tagged_division of I )
assume A1: jauge1 <= jauge2 ; :: thesis: TD is jauge2 -fine tagged_division of I
consider D being Division of I, T being Element of set_of_tagged_Division D such that
A2: TD = [D,T] and
A3: for i being Nat st i in dom D holds
vol (divset (D,i)) <= jauge1 . (T . i) by COUSIN:def 4;

now :: thesis: for i being Nat st i in dom D holds
vol (divset (D,i)) <= jauge2 . (T . i)

let i be Nat; :: thesis: ( i in dom D implies vol (divset (D,i)) <= jauge2 . (T . i) )
assume A4: i in dom D ; :: thesis: vol (divset (D,i)) <= jauge2 . (T . i)
then A5: vol (divset (D,i)) <= jauge1 . (T . i) by A3;
dom T = Seg (len T) by FINSEQ_1:def 3
.= Seg (len (tagged_of TD)) by A2, Th20
.= Seg (len (division_of TD)) by Th21
.= Seg (len D) by A2, Th20
.= dom D by FINSEQ_1:def 3 ;
then A6: T . i in rng T by A4, FUNCT_1:3;
rng T c= I by Th22;
then jauge1 . (T . i) <= jauge2 . (T . i) by A6, A1;
hence vol (divset (D,i)) <= jauge2 . (T . i) by A5, XXREAL_0:2; :: thesis: verum

end;

hence TD is jauge2 -fine tagged_division of I by A2, COUSIN:def 4; :: thesis: verum