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-min 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: W-min P = |[(- 1),0]|
then A3: W-bound P = - 1 by Lm4;
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: NW-corner P = |[(- 1),1]| by A3, PSCOMP_1:def 12;
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: SW-corner P = |[(- 1),(- 1)]| by A3, PSCOMP_1:def 11;
A7: (LSeg ((SW-corner P),(NW-corner P))) /\ P c= {|[(- 1),0]|}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg ((SW-corner P),(NW-corner P))) /\ P or x in {|[(- 1),0]|} )
assume A8: x in (LSeg ((SW-corner P),(NW-corner P))) /\ P ; :: thesis: x in {|[(- 1),0]|}
then A9: x in { (((1 - l) * (SW-corner P)) + (l * (NW-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) * (SW-corner P)) + (l * (NW-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) * (- 1)) + (l * (- 1))),(((1 - l) * (- 1)) + (l * 1))]| by EUCLID:56;
then q3 `1 = - 1 by EUCLID:52;
then A13: 1 = sqrt (((- 1) ^2) + ((q3 `2) ^2)) by A10, JGRAPH_3:1
.= sqrt (1 + ((q3 `2) ^2)) ;

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

assume (q3 `2) ^2 > 0 ; :: thesis: contradiction
then 1 < 1 + ((q3 `2) ^2) by XREAL_1:29;
hence contradiction by A13, SQUARE_1:18, SQUARE_1:27; :: 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 ((SW-corner P),(NW-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 ((SW-corner P),(NW-corner P))) /\ P )
assume x in {|[(- 1),0]|} ; :: thesis: x in (LSeg ((SW-corner P),(NW-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 ((SW-corner P),(NW-corner P)) by A6, A5, A15;
hence x in (LSeg ((SW-corner P),(NW-corner P))) /\ P by A16, XBOOLE_0:def 4; :: thesis: verum

end;

then (LSeg ((SW-corner P),(NW-corner P))) /\ P = {|[(- 1),0]|} by A7, XBOOLE_0:def 10;
then A17: W-most P = {|[(- 1),0]|} by PSCOMP_1:def 15;
(proj2 | (W-most P)) .: the carrier of ((TOP-REAL 2) | (W-most P)) = (proj2 | (W-most P)) .: (W-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 lower_bound ((proj2 | (W-most P)) .: the carrier of ((TOP-REAL 2) | (W-most P))) = 0 by SEQ_4:9;
then lower_bound (proj2 | (W-most P)) = 0 by PSCOMP_1:def 1;
hence W-min P = |[(- 1),0]| by A3, PSCOMP_1:def 19; :: thesis: verum