let C be Chain of X; :: thesis: ( C = NAT --> x implies ( C is ascending & C is stagnating ) )
assume A1: C = NAT --> x ; :: thesis: ( C is ascending & C is stagnating )

hereby :: according to RING_2:def 1 :: thesis: C is stagnating

let i be Nat; :: thesis: C . i c= C . (i + 1)
( C . i = x & C . (i + 1) = x ) by A1, FUNCOP_1:7, ORDINAL1:def 12;
hence C . i c= C . (i + 1) ; :: thesis: verum

end;

take 0 ; :: according to RING_2:def 2 :: thesis: for j being Nat st j >= 0 holds
C . j = C . 0
let j be Nat; :: thesis: ( j >= 0 implies C . j = C . 0 )
( C . 0 = x & C . j = x ) by A1, FUNCOP_1:7, ORDINAL1:def 12;
hence ( j >= 0 implies C . j = C . 0 ) ; :: thesis: verum