let L be reflexive with_suprema RelStr ; :: thesis: ( L is up-complete implies L is upper-bounded )

assume A1: L is up-complete ; :: thesis: L is upper-bounded

[#] L = the carrier of L ;

then ex x being Element of L st

( x is_>=_than the carrier of L & ( for y being Element of L st y is_>=_than the carrier of L holds

x <= y ) ) by A1;

hence ex x being Element of L st x is_>=_than the carrier of L ; :: according to YELLOW_0:def 5 :: thesis: verum

assume A1: L is up-complete ; :: thesis: L is upper-bounded

[#] L = the carrier of L ;

then ex x being Element of L st

( x is_>=_than the carrier of L & ( for y being Element of L st y is_>=_than the carrier of L holds

x <= y ) ) by A1;

hence ex x being Element of L st x is_>=_than the carrier of L ; :: according to YELLOW_0:def 5 :: thesis: verum