let P be non empty Poset; :: thesis: ( P is flat implies P is lower-bounded )
assume P is flat ; :: thesis: P is lower-bounded
then consider a being Element of P such that
A1: for x, y being Element of P holds
( x <= y iff ( x = a or x = y ) ) ;
take a ; :: according to YELLOW_0:def 4 :: thesis: a is_<=_than the carrier of P
thus a is_<=_than the carrier of P by A1; :: thesis: verum