let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } implies W-bound P = - 1 )
assume P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } ; :: thesis: W-bound P = - 1
then proj1 .: P = [.(- 1),1.] by Lm3;
then (proj1 | P) .: P = [.(- 1),1.] by RELAT_1:129;
then ( the carrier of ((TOP-REAL 2) | P) = P & lower_bound ((proj1 | P) .: P) = - 1 ) by JORDAN5A:19, PRE_TOPC:8;
then lower_bound (proj1 | P) = - 1 by PSCOMP_1:def 1;
hence W-bound P = - 1 by PSCOMP_1:def 7; :: thesis: verum