let X be non empty set ; :: thesis: ( InclPoset X is upper-bounded implies union X in X )
assume InclPoset X is upper-bounded ; :: thesis: union X in X
then consider x being Element of (InclPoset X) such that
A1: x is_>=_than the carrier of (InclPoset X) by YELLOW_0:def 5;

now :: thesis: for y being object st y in union X holds
y in x

let y be object ; :: thesis: ( y in union X implies y in x )
assume y in union X ; :: thesis: y in x
then consider Y being set such that
A2: y in Y and
A3: Y in X by TARSKI:def 4;
reconsider Y = Y as Element of (InclPoset X) by A3;
Y <= x by A1;
then Y c= x by Th3;
hence y in x by A2; :: thesis: verum

end;

then A4: union X c= x ;
( x in X & x c= union X ) by ZFMISC_1:74;
hence union X in X by A4, XBOOLE_0:def 10; :: thesis: verum