let X, Y be Subset of REAL; :: thesis: ( Y is bounded_below & X <> {} & ( for r being Real st r in X holds
ex r1 being Real st
( r1 in Y & r1 <= r ) ) implies lower_bound X >= lower_bound Y )
assume that
A1: Y is bounded_below and
A2: X <> {} and
A3: for r being Real st r in X holds
ex r1 being Real st
( r1 in Y & r1 <= r ) ; :: thesis: lower_bound X >= lower_bound Y
now :: thesis: for r1 being Real st r1 in X holds
r1 >= lower_bound Y
let r1 be Real; :: thesis: ( r1 in X implies r1 >= lower_bound Y )
assume r1 in X ; :: thesis: r1 >= lower_bound Y
then consider r2 being Real such that
A4: r2 in Y and
A5: r2 <= r1 by A3;
lower_bound Y <= r2 by A1, A4, Def2;
hence r1 >= lower_bound Y by A5, XXREAL_0:2; :: thesis: verum
end;
hence lower_bound X >= lower_bound Y by A2, Th112; :: thesis: verum