for R being non empty connected Poset st R is well_founded holds
FinPoset R is well_founded