let X be Subset of REAL ; :: thesis: ( X is bounded & not X is empty implies ( ex r, p being real number st
( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X ) )
assume that
A1: X is bounded and
A2: not X is empty ; :: thesis: ( ex r, p being real number st
( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X )
thus ( ex r, p being real number st
( r in X & p in X & p <> r ) implies lower_bound X < upper_bound X ) :: thesis: ( lower_bound X < upper_bound X implies ex r, p being real number st
( r in X & p in X & p <> r ) )

proof

given r, p being real number such that A3: r in X and
A4: p in X and
A5: p <> r ; :: thesis: lower_bound X < upper_bound X

A6: now

assume A7: p < r ; :: thesis: lower_bound X < upper_bound X
lower_bound X <= p by A1, A4, Def5;
then A8: lower_bound X < r by A7, XXREAL_0:2;
r <= upper_bound X by A1, A3, Def4;
hence lower_bound X < upper_bound X by A8, XXREAL_0:2; :: thesis: verum

end;

now

assume A9: r < p ; :: thesis: lower_bound X < upper_bound X
lower_bound X <= r by A3, Def5, A1;
then A10: lower_bound X < p by A9, XXREAL_0:2;
p <= upper_bound X by A4, Def4, A1;
hence lower_bound X < upper_bound X by A10, XXREAL_0:2; :: thesis: verum

end;

hence lower_bound X < upper_bound X by A5, A6, XXREAL_0:1; :: thesis: verum

end;

assume that
A11: lower_bound X < upper_bound X and
A12: for r, p being real number st r in X & p in X holds
p = r ; :: thesis: contradiction
consider r being Element of REAL such that
A13: r in X by A2, SUBSET_1:10;
for x being set holds
( x in X iff x = r ) by A12, A13;
then X = {r} by TARSKI:def 1;
hence contradiction by A11, Th23; :: thesis: verum