let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A holds D in set_of_tagged_Division D
let D be Division of A; :: thesis: D in set_of_tagged_Division D
for i being Nat st i in dom D holds
D . i in divset (D,i)

proof

let i be Nat; :: thesis: ( i in dom D implies D . i in divset (D,i) )
assume A1: i in dom D ; :: thesis: D . i in divset (D,i)
consider a, b being Real such that
A2: divset (D,i) = [.a,b.] by MEASURE5:def 3;
a <= b by A2, XXREAL_1:29;
then A3: ( upper_bound (divset (D,i)) = b & b in [.a,b.] ) by A2, JORDAN5A:19, XXREAL_1:1;
1 <= i by A1, FINSEQ_3:25;

per cases then ( i = 1 or 1 < i ) by XXREAL_0:1;

suppose i = 1 ; :: thesis: D . i in divset (D,i)

hence D . i in divset (D,i) by A3, A2, A1, INTEGRA1:def 4; :: thesis: verum

end;

suppose 1 < i ; :: thesis: D . i in divset (D,i)

hence D . i in divset (D,i) by A3, A2, A1, INTEGRA1:def 4; :: thesis: verum

end;

end;

end;

hence D in set_of_tagged_Division D by Def2; :: thesis: verum