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 )

( 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

( 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 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 ) ) )

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;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

( 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