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