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

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 Def17;
hence X c= the carrier of A ; :: thesis: verum

end;

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