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