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

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