theorem Th33: :: BAGORDER:36

for R being non empty connected Poset
for x being Element of Fin the carrier of R st x <> {} holds
not [x,{}] in union (rng (FinOrd-Approx R))