let f be non trivial FinSequence of (TOP-REAL 2); :: thesis: W-min (L~ f) in rng f
set p = W-min (L~ f);
A1: len f >= 2 by REALSET1:13;
W-min (L~ f) in L~ f by SPRECT_1:15;
then consider i being Element of NAT such that
A2: ( 1 <= i & i + 1 <= len f ) and
A3: W-min (L~ f) in LSeg (f /. i),(f /. (i + 1)) by SPPOL_2:14;
i <= i + 1 by NAT_1:11;
then ( i + 1 >= 1 & i <= len f ) by A2, XXREAL_0:2;
then A4: ( i in dom f & i + 1 in dom f ) by A2, FINSEQ_3:27;
then ( f /. i in L~ f & f /. (i + 1) in L~ f ) by A1, GOBOARD1:16;
then A5: ( (f /. i) `1 >= W-bound (L~ f) & (f /. (i + 1)) `1 >= W-bound (L~ f) ) by PSCOMP_1:71;
A6: (W-min (L~ f)) `1 = W-bound (L~ f) by EUCLID:56;

now

per cases ( W-min (L~ f) = f /. i or W-min (L~ f) = f /. (i + 1) or ( (W-min (L~ f)) `1 = (f /. i) `1 & (W-min (L~ f)) `1 = (f /. (i + 1)) `1 ) ) by A3, A5, A6, Th23;

suppose W-min (L~ f) = f /. i ; :: thesis: W-min (L~ f) in rng f

hence W-min (L~ f) in rng f by A4, PARTFUN2:4; :: thesis: verum

end;

suppose W-min (L~ f) = f /. (i + 1) ; :: thesis: W-min (L~ f) in rng f

hence W-min (L~ f) in rng f by A4, PARTFUN2:4; :: thesis: verum

end;

suppose A7: ( (W-min (L~ f)) `1 = (f /. i) `1 & (W-min (L~ f)) `1 = (f /. (i + 1)) `1 ) ; :: thesis: W-min (L~ f) in rng f

then ( f /. i in W-most (L~ f) & f /. (i + 1) in W-most (L~ f) ) by A1, A4, A6, Th16, GOBOARD1:16;
then A8: ( (f /. i) `2 >= (W-min (L~ f)) `2 & (f /. (i + 1)) `2 >= (W-min (L~ f)) `2 ) by PSCOMP_1:88;
( (f /. i) `2 <= (f /. (i + 1)) `2 or (f /. (i + 1)) `2 <= (f /. i) `2 ) ;
then ( (f /. i) `2 <= (W-min (L~ f)) `2 or (f /. (i + 1)) `2 <= (W-min (L~ f)) `2 ) by A3, TOPREAL1:10;
then ( (W-min (L~ f)) `2 = (f /. i) `2 or (W-min (L~ f)) `2 = (f /. (i + 1)) `2 ) by A8, XXREAL_0:1;
then ( W-min (L~ f) = f /. i or W-min (L~ f) = f /. (i + 1) ) by A7, TOPREAL3:11;
hence W-min (L~ f) in rng f by A4, PARTFUN2:4; :: thesis: verum

end;

end;

end;

hence W-min (L~ f) in rng f ; :: thesis: verum