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