let X be non empty real-membered set ; :: thesis: for r being Real st ( for s being Real st s in X holds
s <= r ) & ( for t being Real st ( for s being Real st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X
let r be Real; :: thesis: ( ( for s being Real st s in X holds
s <= r ) & ( for t being Real st ( for s being Real st s in X holds
s <= t ) holds
r <= t ) implies r = upper_bound X )
assume that
A1: for s being Real st s in X holds
s <= r and
A2: for t being Real st ( for s being Real st s in X holds
s <= t ) holds
r <= t ; :: thesis: r = upper_bound X
A3: now :: thesis: for s being Real st 0 < s holds
ex t being Real st
( t in X & not r - s >= t )
let s be Real; :: thesis: ( 0 < s implies ex t being Real st
( t in X & not r - s >= t ) )
assume A4: 0 < s ; :: thesis: ex t being Real st
( t in X & not r - s >= t )
assume for t being Real st t in X holds
r - s >= t ; :: thesis: contradiction
then r <= r - s by A2;
then r + s <= r by XREAL_1:19;
hence contradiction by A4, XREAL_1:29; :: thesis: verum
end;
X is bounded_above
proof
take r ; :: according to XXREAL_2:def 10 :: thesis: r is UpperBound of X
let s be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not s in X or s <= r )
assume s in X ; :: thesis: s <= r
hence s <= r by A1; :: thesis: verum
end;
hence r = upper_bound X by A1, A3, Def1; :: thesis: verum