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 upper-bounded )
hereby :: thesis: ( R is upper-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 upper-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 upper-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 5 :: 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