let S be Subset of (TOP-REAL 2); :: thesis: N-bound S = upper_bound (proj2 .: S)
thus N-bound S = upper_bound (rng (proj2 | S)) by FUNCT_2:45
.= upper_bound (proj2 .: S) by RELAT_1:148 ; :: thesis: verum