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