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) ;
A1: "/\" {} ,(InclPoset X) c= a by ZFMISC_1:92;
A2: {} is_>=_than a by YELLOW_0:6;

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:92;
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 ex_inf_of {} , InclPoset X by YELLOW_0:43;
then a <= "/\" {} ,(InclPoset X) by A2, YELLOW_0:def 10;
then A3: a c= "/\" {} ,(InclPoset X) by Th3;
thus Top (InclPoset X) = "/\" {} ,(InclPoset X) by YELLOW_0:def 12
.= union X by A1, A3, XBOOLE_0:def 10 ; :: thesis: verum