let X be non empty set ; :: thesis: for Y being non empty Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds
union Y c= sup Y
let Y be non empty Subset of (InclPoset X); :: thesis: ( ex_sup_of Y, InclPoset X implies union Y c= sup Y )
assume A1: ex_sup_of Y, InclPoset X ; :: thesis: union Y c= sup Y

now :: thesis: for x being set st x in Y holds
x c= sup Y

let x be set ; :: thesis: ( x in Y implies x c= sup Y )
assume A2: x in Y ; :: thesis: x c= sup Y
then reconsider x1 = x as Element of (InclPoset X) ;
sup Y is_>=_than Y by A1, YELLOW_0:30;
then sup Y >= x1 by A2, LATTICE3:def 9;
hence x c= sup Y by YELLOW_1:3; :: thesis: verum

end;

hence union Y c= sup Y by ZFMISC_1:76; :: thesis: verum