:: deftheorem asc defines ascending RING_2:def 1 :
for X being non empty set
for C being Chain of X holds
( C is ascending iff for i being Nat holds C . i c= C . (i + 1) );