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) ;
for b being Element of (InclPoset X) st b in X holds
b <= a by Th3, ZFMISC_1:74;
then a is_>=_than X ;
then InclPoset X is upper-bounded by YELLOW_0:def 5;
then ( {} is_>=_than a & ex_inf_of {} , InclPoset X ) by 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 ; :: thesis: verum