let S be Subset of ; :: thesis: W-bound S = inf (proj1 .: S)
thus W-bound S = inf (rng (proj1 | S)) by FUNCT_2:45
.= inf (proj1 .: S) by RELAT_1:148 ; :: thesis: verum