let S be Subset of (TOP-REAL 2); :: thesis: W-bound S = lower_bound (proj1 .: S)
thus W-bound S = lower_bound (rng (proj1 | S)) by RELSET_1:22
.= lower_bound (proj1 .: S) by RELAT_1:115 ; :: thesis: verum