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