let A be non empty Subset of R^1; :: thesis: ex X being non empty Subset of REAL st
( A = X & lower_bound A = lower_bound X )
reconsider X = A as non empty Subset of REAL by TOPMETR:17;
take X ; :: thesis: ( A = X & lower_bound A = lower_bound X )
lower_bound A = lower_bound ([#] A) by WEIERSTR:def 3
.= lower_bound X by WEIERSTR:def 1 ;
hence ( A = X & lower_bound A = lower_bound X ) ; :: thesis: verum