theorem Th43: :: ORDERS_2:43

for A being non empty Poset
for f being Choice_Function of (BOOL the carrier of A) holds union (Chains f) <> {}