let R be non empty real RelStr ; :: thesis: ( ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x >= y ) ) iff R is upper-bounded )

hereby :: thesis: ( R is upper-bounded implies ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x >= y ) ) )

given x being real number such that A1: x in the carrier of R and
A2: for y being real number st y in the carrier of R holds
x >= y ; :: thesis: R is upper-bounded
reconsider a = x as Element of R by A1;

now

let b be Element of R; :: thesis: ( b in the carrier of R implies a >>= b )
assume b in the carrier of R ; :: thesis: a >>= b
a >= b by A2;
hence a >>= b by Th3; :: thesis: verum

end;

then a is_>=_than the carrier of R by LATTICE3:def 9;
hence R is upper-bounded by YELLOW_0:def 5; :: thesis: verum

end;

given x being Element of R such that A3: x is_>=_than the carrier of R ; :: according to YELLOW_0:def 5 :: thesis: ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x >= y ) )
take x ; :: thesis: ( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x >= y ) )
thus x in the carrier of R ; :: thesis: for y being real number st y in the carrier of R holds
x >= y
let y be real number ; :: thesis: ( y in the carrier of R implies x >= y )
assume y in the carrier of R ; :: thesis: x >= y
then reconsider b = y as Element of R ;
x >>= b by A3, LATTICE3:def 9;
hence x >= y by Th3; :: thesis: verum