let T be Element of set_of_tagged_Division D; :: thesis: not T is empty
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