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 E-max P = |[1,0 ]| )
A1: the carrier of ((TOP-REAL 2) | P) = P by PRE_TOPC:29;
assume A2: P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } ; :: thesis: E-max P = |[1,0 ]|
then A3: E-bound P = 1 by Th31;
proj2 .: P = [.(- 1),1.] by A2, Lm3;
then A4: (proj2 | P) .: P = [.(- 1),1.] by RELAT_1:162;
then upper_bound ((proj2 | P) .: P) = 1 by JORDAN5A:20;
then upper_bound (proj2 | P) = 1 by A1, PSCOMP_1:def 21;
then N-bound P = 1 by PSCOMP_1:def 31;
then A5: NE-corner P = |[1,1]| by A3, PSCOMP_1:def 36;
lower_bound ((proj2 | P) .: P) = - 1 by A4, JORDAN5A:20;
then lower_bound (proj2 | P) = - 1 by A1, PSCOMP_1:def 20;
then S-bound P = - 1 by PSCOMP_1:def 33;
then A6: SE-corner P = |[1,(- 1)]| by A3, PSCOMP_1:def 37;
A7: (LSeg (SE-corner P),(NE-corner P)) /\ P c= {|[1,0 ]|}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (SE-corner P),(NE-corner P)) /\ P or x in {|[1,0 ]|} )
assume A8: x in (LSeg (SE-corner P),(NE-corner P)) /\ P ; :: thesis: x in {|[1,0 ]|}
then A9: x in { (((1 - l) * (SE-corner P)) + (l * (NE-corner P))) where l is Real : ( 0 <= l & l <= 1 ) } by XBOOLE_0:def 4;
x in P by A8, XBOOLE_0:def 4;
then A10: ex q2 being Point of (TOP-REAL 2) st
( q2 = x & |.q2.| = 1 ) by A2;
consider l being Real such that
A11: x = ((1 - l) * (SE-corner P)) + (l * (NE-corner P)) and
0 <= l and
l <= 1 by A9;
reconsider q3 = x as Point of (TOP-REAL 2) by A11;
x = |[((1 - l) * 1),((1 - l) * (- 1))]| + (l * |[1,1]|) by A6, A5, A11, EUCLID:62;
then x = |[((1 - l) * 1),((1 - l) * (- 1))]| + |[(l * 1),(l * 1)]| by EUCLID:62;
then A12: x = |[(((1 - l) + l) * 1),(((1 - l) * (- 1)) + (l * 1))]| by EUCLID:60;
then A13: q3 `1 = 1 by EUCLID:56;

now

assume (q3 `2 ) ^2 > 0 ; :: thesis: contradiction
then 1 ^2 < 1 + ((q3 `2 ) ^2 ) by XREAL_1:31;
hence contradiction by A13, A10, JGRAPH_3:10; :: thesis: verum

end;

then (q3 `2 ) ^2 = 0 by XREAL_1:65;
then A14: q3 `2 = 0 by XCMPLX_1:6;
q3 `2 = ((1 - l) * (- 1)) + l by A12, EUCLID:56;
hence x in {|[1,0 ]|} by A12, A14, TARSKI:def 1; :: thesis: verum

end;

{|[1,0 ]|} c= (LSeg (SE-corner P),(NE-corner P)) /\ P

proof

set q = |[1,0 ]|;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {|[1,0 ]|} or x in (LSeg (SE-corner P),(NE-corner P)) /\ P )
assume x in {|[1,0 ]|} ; :: thesis: x in (LSeg (SE-corner P),(NE-corner P)) /\ P
then A15: x = |[1,0 ]| by TARSKI:def 1;
( |[1,0 ]| `2 = 0 & |[1,0 ]| `1 = 1 ) by EUCLID:56;
then |.|[1,0 ]|.| = sqrt ((1 ^2 ) + (0 ^2 )) by JGRAPH_3:10
.= 1 by SQUARE_1:83 ;
then A16: x in P by A2, A15;
|[1,0 ]| = |[(((1 / 2) * 1) + ((1 / 2) * 1)),(((1 / 2) * (- 1)) + ((1 / 2) * 1))]| ;
then |[1,0 ]| = |[((1 / 2) * 1),((1 / 2) * (- 1))]| + |[((1 / 2) * 1),((1 / 2) * 1)]| by EUCLID:60;
then |[1,0 ]| = |[((1 / 2) * 1),((1 / 2) * (- 1))]| + ((1 / 2) * |[1,1]|) by EUCLID:62;
then |[1,0 ]| = ((1 / 2) * |[1,(- 1)]|) + ((1 - (1 / 2)) * |[1,1]|) by EUCLID:62;
then x in LSeg (SE-corner P),(NE-corner P) by A6, A5, A15;
hence x in (LSeg (SE-corner P),(NE-corner P)) /\ P by A16, XBOOLE_0:def 4; :: thesis: verum

end;

then (LSeg (SE-corner P),(NE-corner P)) /\ P = {|[1,0 ]|} by A7, XBOOLE_0:def 10;
then A17: E-most P = {|[1,0 ]|} by PSCOMP_1:def 40;
(proj2 | (E-most P)) .: the carrier of ((TOP-REAL 2) | (E-most P)) = (proj2 | (E-most P)) .: (E-most P) by PRE_TOPC:29
.= Im proj2 ,|[1,0 ]| by A17, RELAT_1:162
.= {(proj2 . |[1,0 ]|)} by SETWISEO:13
.= {(|[1,0 ]| `2 )} by PSCOMP_1:def 29
.= {0 } by EUCLID:56 ;
then upper_bound ((proj2 | (E-most P)) .: the carrier of ((TOP-REAL 2) | (E-most P))) = 0 by SEQ_4:22;
then upper_bound (proj2 | (E-most P)) = 0 by PSCOMP_1:def 21;
hence E-max P = |[1,0 ]| by A3, PSCOMP_1:def 46; :: thesis: verum