let X be non empty real-membered set ; :: thesis: for r, t being real number st ( for s being real number st s in X holds
s <= t ) holds
upper_bound X <= t
let r be real number ; :: thesis: for t being real number st ( for s being real number st s in X holds
s <= t ) holds
upper_bound X <= t
set r = upper_bound X;
let t be real number ; :: thesis: ( ( for s being real number st s in X holds
s <= t ) implies upper_bound X <= t )
assume A1: for s being real number st s in X holds
s <= t ; :: thesis: upper_bound X <= t
then A2: X is bounded_above by Def1;
set s = (upper_bound X) - t;
assume upper_bound X > t ; :: thesis: contradiction
then (upper_bound X) - t > 0 by XREAL_1:52;
then consider t' being real number such that
A3: ( t' in X & (upper_bound X) - ((upper_bound X) - t) < t' ) by A2, Def4;
thus contradiction by A1, A3; :: thesis: verum