theorem Th35: :: BAGORDER:38

for R being non empty connected Poset holds union (rng (FinOrd-Approx R)) is Order of (Fin the carrier of R)