:: deftheorem defines FinOrd BAGORDER:def 15 :
for R being non empty connected Poset holds FinOrd R = union (rng (FinOrd-Approx R));