let L be non empty reflexive RelStr ; :: thesis: ( L is /\-complete implies L is lower-bounded )
assume L is /\-complete ; :: thesis: L is lower-bounded
then ex x being Element of L st
( x is_<=_than [#] L & ( for y being Element of L st y is_<=_than [#] L holds
x >= y ) ) ;
hence ex x being Element of L st x is_<=_than the carrier of L ; :: according to YELLOW_0:def 4 :: thesis: verum