let X be non empty real-membered set ; :: thesis: for r, t being Real st ( for s being Real st s in X holds
s <= t ) holds
upper_bound X <= t
let r be Real; :: thesis: for t being Real st ( for s being Real st s in X holds
s <= t ) holds
upper_bound X <= t
set r = upper_bound X;
let t be Real; :: thesis: ( ( for s being Real st s in X holds
s <= t ) implies upper_bound X <= t )
assume A1: for s being Real st s in X holds
s <= t ; :: thesis: upper_bound X <= t
set s = (upper_bound X) - t;
assume upper_bound X > t ; :: thesis: contradiction
then A2: (upper_bound X) - t > 0 by XREAL_1:50;
X is bounded_above

proof

take t ; :: according to XXREAL_2:def 10 :: thesis: t is UpperBound of X
let s be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not s in X or s <= t )
thus ( not s in X or s <= t ) by A1; :: thesis: verum

end;

then ex t9 being Real st
( t9 in X & (upper_bound X) - ((upper_bound X) - t) < t9 ) by A2, Def1;
hence contradiction by A1; :: thesis: verum