let R be non empty real RelStr ; :: thesis: ( ex x being Real st
( x in the carrier of R & ( for y being Real 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 st
( x in the carrier of R & ( for y being Real st y in the carrier of R holds
x <= y ) ) )

given x being Real such that A1: x in the carrier of R and
A2: for y being Real st y in the carrier of R holds
x <= y ; :: thesis: R is lower-bounded
reconsider a = x as Element of R by A1;
for b being Element of R st b in the carrier of R holds
a <<= b by A2, Th3;
then a is_<=_than the carrier of R ;
hence R is lower-bounded ; :: 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 st
( x in the carrier of R & ( for y being Real st y in the carrier of R holds
x <= y ) )
take x ; :: thesis: ( x in the carrier of R & ( for y being Real st y in the carrier of R holds
x <= y ) )
thus x in the carrier of R ; :: thesis: for y being Real st y in the carrier of R holds
x <= y
let y be Real; :: 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;
hence x <= y by Th3; :: thesis: verum