let A be non empty Poset; :: thesis: for f being Choice_Function of (BOOL the carrier of A) holds union (Chains f) is Subset of A
let f be Choice_Function of (BOOL the carrier of A); :: thesis: union (Chains f) is Subset of A

now :: thesis: for X being set st X in Chains f holds
X c= the carrier of A

let X be set ; :: thesis: ( X in Chains f implies X c= the carrier of A )
assume X in Chains f ; :: thesis: X c= the carrier of A
then X is Chain of f by Def13;
hence X c= the carrier of A ; :: thesis: verum

end;

hence union (Chains f) is Subset of A by ZFMISC_1:76; :: thesis: verum