let f be non trivial FinSequence of (TOP-REAL 2); :: thesis: S-min (L~ f) in rng f
set p = S-min (L~ f);
A1: len f >= 2 by REALSET1:13;
S-min (L~ f) in L~ f by SPRECT_1:14;
then consider i being Element of NAT such that
A2: ( 1 <= i & i + 1 <= len f ) and
A3: S-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) `2 >= S-bound (L~ f) & (f /. (i + 1)) `2 >= S-bound (L~ f) ) by PSCOMP_1:71;
A6: (S-min (L~ f)) `2 = S-bound (L~ f) by EUCLID:56;

now

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

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

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

end;

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

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

end;

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

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

end;

end;

end;

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