let I be non empty closed_interval Subset of REAL; :: thesis: for D being Division of I
for T being Element of set_of_tagged_Division D holds not T is empty
let D be Division of I; :: thesis: for T being Element of set_of_tagged_Division D holds not T is empty
let T be Element of set_of_tagged_Division D; :: thesis: not T is empty
not set_of_tagged_Division D is empty by Th34;
then consider s being non empty non-decreasing FinSequence of REAL such that
A1: T = s and
dom s = dom D and
for i being Nat st i in dom s holds
s . i in divset (D,i) by Def2;
thus not T is empty by A1; :: thesis: verum