let S be non empty antisymmetric RelStr ; :: thesis: ( ex_sup_of {} ,S implies S is lower-bounded )
assume A1: ex_sup_of {} ,S ; :: thesis: S is lower-bounded
take Bottom S ; :: according to YELLOW_0:def 4 :: thesis: Bottom S is_<=_than the carrier of S
let x be Element of S; :: according to LATTICE3:def 8 :: thesis: ( not x in the carrier of S or Bottom S <= x )
{} is_<=_than x ;
hence ( not x in the carrier of S or Bottom S <= x ) by A1, YELLOW_0:30; :: thesis: verum