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 Th78;
then {(f . the carrier of A)} in Chains f by Def17;
hence union (Chains f) <> {} by ORDERS_1:91; :: thesis: verum