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 lower-bounded )

hereby :: thesis: ( R is lower-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 lower-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
b >= a by A2;
hence a <<= b by Th3; :: thesis: verum

end;

then a is_<=_than the carrier of R by LATTICE3:def 8;
hence R is lower-bounded by YELLOW_0:def 4; :: thesis: verum

end;

given x being Element of R such that A3: x is_<=_than the carrier of R ; :: according to YELLOW_0:def 4 :: 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 8;
hence x <= y by Th3; :: thesis: verum