:: deftheorem defines stagnating RING_2:def 2 :
for X being non empty set
for C being Chain of X holds
( C is stagnating iff ex i being Nat st
for j being Nat st j >= i holds
C . j = C . i );