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 & E-bound P = 1 & S-bound P = - 1 & N-bound P = 1 ) )
A1: the carrier of ((TOP-REAL 2) | P) = P by PRE_TOPC:8;
assume A2: P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } ; :: thesis: ( W-bound P = - 1 & E-bound P = 1 & S-bound P = - 1 & N-bound P = 1 )
hence W-bound P = - 1 by Lm4; :: thesis: ( E-bound P = 1 & S-bound P = - 1 & N-bound P = 1 )
proj1 .: P = [.(- 1),1.] by A2, Lm3;
then (proj1 | P) .: P = [.(- 1),1.] by RELAT_1:129;
then upper_bound ((proj1 | P) .: the carrier of ((TOP-REAL 2) | P)) = 1 by A1, JORDAN5A:19;
then upper_bound (proj1 | P) = 1 by PSCOMP_1:def 2;
hence E-bound P = 1 by PSCOMP_1:def 9; :: thesis: ( S-bound P = - 1 & N-bound P = 1 )
proj2 .: P = [.(- 1),1.] by A2, Lm3;
then A3: (proj2 | P) .: P = [.(- 1),1.] by RELAT_1:129;
then lower_bound ((proj2 | P) .: P) = - 1 by JORDAN5A:19;
then lower_bound (proj2 | P) = - 1 by A1, PSCOMP_1:def 1;
hence S-bound P = - 1 by PSCOMP_1:def 10; :: thesis: N-bound P = 1
upper_bound ((proj2 | P) .: P) = 1 by A3, JORDAN5A:19;
then upper_bound (proj2 | P) = 1 by A1, PSCOMP_1:def 2;
hence N-bound P = 1 by PSCOMP_1:def 8; :: thesis: verum