theorem :: RING_2:3

for X being non empty set
for C being ascending Chain of X
for i, j being Nat st i <= j holds
C . i c= C . j by ch1;