let X be non empty set ; :: thesis: ( {} in X implies Bottom (InclPoset X) = {} )
assume {} in X ; :: thesis: Bottom (InclPoset X) = {}
then reconsider a = {} as Element of (InclPoset X) ;
for b being Element of (InclPoset X) st b in X holds
a <= b by Th3, XBOOLE_1:2;
then a is_<=_than X ;
then InclPoset X is lower-bounded by YELLOW_0:def 4;
then ( {} is_<=_than a & ex_sup_of {} , InclPoset X ) by YELLOW_0:42;
then "\/" ({},(InclPoset X)) <= a by YELLOW_0:def 9;
then A1: "\/" ({},(InclPoset X)) c= a by Th3;
thus Bottom (InclPoset X) = "\/" ({},(InclPoset X)) by YELLOW_0:def 11
.= {} by A1 ; :: thesis: verum