consider D being Division of A, T being Element of set_of_tagged_Division D such that
A1: TD = [D,T] by COUSIN:def 3;
ex s being non empty non-decreasing FinSequence of REAL st
( T = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) by COUSIN:def 2;
hence ex b₁ being non empty non-decreasing FinSequence of REAL ex D being Division of A ex T being Element of set_of_tagged_Division D st
( b₁ = T & TD = [D,T] ) by A1; :: thesis: verum