let X be non empty set ; :: thesis: ( union X in X implies Top (InclPoset X) = union X )
assume union X in X ; :: thesis: Top (InclPoset X) = union X
then reconsider a = union X as Element of (InclPoset X) ;

now

let b be Element of (InclPoset X); :: thesis: ( b in X implies b <= a )
assume b in X ; :: thesis: b <= a
b c= union X by ZFMISC_1:74;
hence b <= a by Th3; :: thesis: verum

end;

then a is_>=_than X by LATTICE3:def 9;
then InclPoset X is upper-bounded by YELLOW_0:def 5;
then ( {} is_>=_than a & ex_inf_of {} , InclPoset X ) by YELLOW_0:6, YELLOW_0:43;
then a <= "/\" ({},(InclPoset X)) by YELLOW_0:def 10;
then A1: ( "/\" ({},(InclPoset X)) c= a & a c= "/\" ({},(InclPoset X)) ) by Th3, ZFMISC_1:74;
thus Top (InclPoset X) = "/\" ({},(InclPoset X)) by YELLOW_0:def 12
.= union X by A1, XBOOLE_0:def 10 ; :: thesis: verum