for R being non empty RelStr holds
( R is well_founded iff for f being sequence of R holds not f is descending )