let X be Subset of REAL; :: thesis: ( X is real-bounded & not X is empty implies ( ex r, p being Real st
( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X ) )
assume that
A1: X is real-bounded and
A2: not X is empty ; :: thesis: ( ex r, p being Real st
( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X )
thus ( ex r, p being Real 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 st
( r in X & p in X & p <> r ) )
proof
given r, p being Real such that A3: r in X and
A4: p in X and
A5: p <> r ; :: thesis: lower_bound X < upper_bound X
A6: now :: thesis: ( r < p implies lower_bound X < upper_bound X )
assume A7: r < p ; :: thesis: lower_bound X < upper_bound X
lower_bound X <= r by A1, A3, Def2;
then A8: lower_bound X < p by A7, XXREAL_0:2;
p <= upper_bound X by A1, A4, Def1;
hence lower_bound X < upper_bound X by A8, XXREAL_0:2; :: thesis: verum
end;
now :: thesis: ( p < r implies lower_bound X < upper_bound X )
assume A9: p < r ; :: thesis: lower_bound X < upper_bound X
lower_bound X <= p by A1, A4, Def2;
then A10: lower_bound X < r by A9, XXREAL_0:2;
r <= upper_bound X by A1, A3, Def1;
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;
consider r being Element of REAL such that
A11: r in X by A2;
assume that
A12: lower_bound X < upper_bound X and
A13: for r, p being Real st r in X & p in X holds
p = r ; :: thesis: contradiction
for x being object holds
( x in X iff x = r ) by A13, A11;
then X = {r} by TARSKI:def 1;
hence contradiction by A12, Th10; :: thesis: verum