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 ) )
assume A1: 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 Lm3; :: thesis: ( E-bound P = 1 & S-bound P = - 1 & N-bound P = 1 )
A2: the carrier of ((TOP-REAL 2) | P) = P by PRE_TOPC:29;
proj1 .: P = [.(- 1),1.] by A1, Lm2;
then (proj1 | P) .: P = [.(- 1),1.] by RELAT_1:162;
then (proj1 | P) .: P = [.(- 1),1.] ;
then sup ((proj1 | P) .: the carrier of ((TOP-REAL 2) | P)) = 1 by A2, JORDAN5A:20;
then sup (proj1 | P) = 1 by PSCOMP_1:def 21;
hence E-bound P = 1 by PSCOMP_1:def 32; :: thesis: ( S-bound P = - 1 & N-bound P = 1 )
proj2 .: P = [.(- 1),1.] by A1, Lm2;
then (proj2 | P) .: P = [.(- 1),1.] by RELAT_1:162;
then A3: (proj2 | P) .: P = [.(- 1),1.] ;
then lower_bound ((proj2 | P) .: P) = - 1 by JORDAN5A:20;
then inf (proj2 | P) = - 1 by A2, PSCOMP_1:def 20;
hence S-bound P = - 1 by PSCOMP_1:def 33; :: thesis: N-bound P = 1
sup ((proj2 | P) .: P) = 1 by A3, JORDAN5A:20;
then sup (proj2 | P) = 1 by A2, PSCOMP_1:def 21;
hence N-bound P = 1 by PSCOMP_1:def 31; :: thesis: verum