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:8;
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 Th28;
proj2 .: P = [.(- 1),1.] by A2, Lm3;
then A4: (proj2 | P) .: P = [.(- 1),1.] by RELAT_1:129;
then upper_bound ((proj2 | P) .: P) = 1 by JORDAN5A:19;
then upper_bound (proj2 | P) = 1 by A1, PSCOMP_1:def 2;
then N-bound P = 1 by PSCOMP_1:def 8;
then A5: NE-corner P = |[1,1]| by A3, PSCOMP_1:def 13;
lower_bound ((proj2 | P) .: P) = - 1 by A4, JORDAN5A:19;
then lower_bound (proj2 | P) = - 1 by A1, PSCOMP_1:def 1;
then S-bound P = - 1 by PSCOMP_1:def 10;
then A6: SE-corner P = |[1,(- 1)]| by A3, PSCOMP_1:def 14;
A7: (LSeg ((SE-corner P),(NE-corner P))) /\ P c= {|[1,0]|}

proof

let x be object ; :: 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:58;
then x = |[((1 - l) * 1),((1 - l) * (- 1))]| + |[(l * 1),(l * 1)]| by EUCLID:58;
then A12: x = |[(((1 - l) + l) * 1),(((1 - l) * (- 1)) + (l * 1))]| by EUCLID:56;
then A13: q3 `1 = 1 by EUCLID:52;

now :: thesis: not (q3 `2) ^2 > 0

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

end;

then (q3 `2) ^2 = 0 by XREAL_1:63;
then A14: q3 `2 = 0 by XCMPLX_1:6;
q3 `2 = ((1 - l) * (- 1)) + l by A12, EUCLID:52;
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 object ; :: 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:52;
then |.|[1,0]|.| = sqrt ((1 ^2) + (0 ^2)) by JGRAPH_3:1
.= 1 ;
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:56;
then |[1,0]| = |[((1 / 2) * 1),((1 / 2) * (- 1))]| + ((1 / 2) * |[1,1]|) by EUCLID:58;
then |[1,0]| = ((1 / 2) * |[1,(- 1)]|) + ((1 - (1 / 2)) * |[1,1]|) by EUCLID:58;
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 17;
(proj2 | (E-most P)) .: the carrier of ((TOP-REAL 2) | (E-most P)) = (proj2 | (E-most P)) .: (E-most P) by PRE_TOPC:8
.= Im (proj2,|[1,0]|) by A17, RELAT_1:129
.= {(proj2 . |[1,0]|)} by SETWISEO:8
.= {(|[1,0]| `2)} by PSCOMP_1:def 6
.= {0} by EUCLID:52 ;
then upper_bound ((proj2 | (E-most P)) .: the carrier of ((TOP-REAL 2) | (E-most P))) = 0 by SEQ_4:9;
then upper_bound (proj2 | (E-most P)) = 0 by PSCOMP_1:def 2;
hence E-max P = |[1,0]| by A3, PSCOMP_1:def 23; :: thesis: verum