let S be non empty antisymmetric RelStr ; :: thesis: ( ex_inf_of {} ,S implies S is upper-bounded )
assume A1: ex_inf_of {} ,S ; :: thesis: S is upper-bounded
take Top S ; :: according to YELLOW_0:def 5 :: thesis: the carrier of S is_<=_than Top S
let x be Element of S; :: according to LATTICE3:def 9 :: thesis: ( not x in the carrier of S or x <= Top S )
{} is_>=_than x ;
hence ( not x in the carrier of S or x <= Top S ) by A1, YELLOW_0:31; :: thesis: verum