let A be non empty Poset; :: thesis: for f being Choice_Function of (BOOL the carrier of A) holds union (Chains f) <> {}
let f be Choice_Function of (BOOL the carrier of A); :: thesis: union (Chains f) <> {}
{(f . the carrier of A)} is Chain of f by Th36;
then {(f . the carrier of A)} in Chains f by Def13;
hence union (Chains f) <> {} by ORDERS_1:6; :: thesis: verum