:: deftheorem Def2 defines set_of_tagged_Division COUSIN:def 2 :
for A being non empty closed_interval Subset of REAL
for D being Division of A
for b₃ being Subset of (REAL *) holds
( b₃ = set_of_tagged_Division D iff for x being object holds
( x in b₃ iff ex s being non empty non-decreasing FinSequence of REAL st
( x = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) ) );