let n be Nat; :: thesis:
assume A1: S₁[n] ; :: thesis:
let R be finite Subset of REAL; :: thesis:
assume that
A2: R <> {} and
A3: card R = n + 1 ; :: thesis:

now :: thesis:

per cases ;

suppose A4: n = 0 ; :: thesis:

thus R is bounded_above ; :: thesis:
consider x being object such that
A5: R = {x} by A3, A4, CARD_2:42;
x in R by A5, TARSKI:def 1;
then reconsider r = x as Real ;
upper_bound R = r by A5, Th9;
hence upper_bound R in R by A5, TARSKI:def 1; :: thesis:
thus R is bounded_below ; :: thesis:
lower_bound R = r by A5, Th9;
hence lower_bound R in R by A5, TARSKI:def 1; :: thesis:

end;

suppose A6: n <> 0 ; :: thesis:

set x = the Element of R;
reconsider x = the Element of R as Real ;
reconsider X = R \ {x} as finite Subset of REAL ;
set u = upper_bound X;
set m = max (x,(upper_bound X));
set l = lower_bound X;
set mi = min (x,(lower_bound X));
{x} c= R by A2, ZFMISC_1:31;
then card (R \ {x}) = (card R) - (card {x}) by CARD_2:44;
then A7: card X = (n + 1) - 1 by A3, CARD_1:30
.= n ;
then A8: upper_bound X in X by A1, A6, CARD_1:27;

A9: now :: thesis:

reconsider s = max (x,(upper_bound X)) as Real ;
let r be Real; :: thesis:
assume A10: 0 < r ; :: thesis:
take s = s; :: thesis:

now :: thesis:

per cases by XXREAL_0:16;

suppose max (x,(upper_bound X)) = x ; :: thesis:

hence s in R by A2; :: thesis:
thus (max (x,(upper_bound X))) - r < s by A10, XREAL_1:44; :: thesis:

end;

suppose max (x,(upper_bound X)) = upper_bound X ; :: thesis:

hence s in R by A8, XBOOLE_0:def 5; :: thesis:
thus (max (x,(upper_bound X))) - r < s by A10, XREAL_1:44; :: thesis:

end;

end;

end;

hence ( s in R & (max (x,(upper_bound X))) - r < s ) ; :: thesis:

end;

A11: lower_bound X in X by A1, A6, A7, CARD_1:27;

A12: now :: thesis:

reconsider s = min (x,(lower_bound X)) as Real ;
let r be Real; :: thesis:
assume A13: 0 < r ; :: thesis:
take s = s; :: thesis:

now :: thesis:

per cases by XXREAL_0:15;

suppose min (x,(lower_bound X)) = x ; :: thesis:

hence s in R by A2; :: thesis:
thus s < (min (x,(lower_bound X))) + r by A13, XREAL_1:29; :: thesis:

end;

suppose min (x,(lower_bound X)) = lower_bound X ; :: thesis:

hence s in R by A11, XBOOLE_0:def 5; :: thesis:
thus s < (min (x,(lower_bound X))) + r by A13, XREAL_1:29; :: thesis:

end;

end;

end;

hence ( s in R & s < (min (x,(lower_bound X))) + r ) ; :: thesis:

end;

thus R is bounded_above ; :: thesis:
A14: upper_bound X <= max (x,(upper_bound X)) by XXREAL_0:25;

A15: now :: thesis:

let s be Real; :: thesis:
assume A16: s in R ; :: thesis:

now :: thesis:

per cases ;

suppose s = x ; :: thesis:

hence s <= max (x,(upper_bound X)) by XXREAL_0:25; :: thesis:

end;

suppose s <> x ; :: thesis:

then not s in {x} by TARSKI:def 1;
then s in X by A16, XBOOLE_0:def 5;
then s <= upper_bound X by Def1;
hence s <= max (x,(upper_bound X)) by A14, XXREAL_0:2; :: thesis:

end;

end;

end;

hence s <= max (x,(upper_bound X)) ; :: thesis:

end;

now :: thesis:

per cases by XXREAL_0:16;

suppose max (x,(upper_bound X)) = x ; :: thesis:

hence max (x,(upper_bound X)) in R by A2; :: thesis:

end;

suppose max (x,(upper_bound X)) = upper_bound X ; :: thesis:

hence max (x,(upper_bound X)) in R by A8, XBOOLE_0:def 5; :: thesis:

end;

end;

end;

hence upper_bound R in R by A15, A9, Def1; :: thesis:
thus R is bounded_below ; :: thesis:
A17: min (x,(lower_bound X)) <= lower_bound X by XXREAL_0:17;

A18: now :: thesis:

let s be Real; :: thesis:
assume A19: s in R ; :: thesis:

now :: thesis:

per cases ;

suppose s = x ; :: thesis:

hence min (x,(lower_bound X)) <= s by XXREAL_0:17; :: thesis:

end;

suppose s <> x ; :: thesis:

then not s in {x} by TARSKI:def 1;
then s in X by A19, XBOOLE_0:def 5;
then lower_bound X <= s by Def2;
hence min (x,(lower_bound X)) <= s by A17, XXREAL_0:2; :: thesis:

end;

end;

end;

hence min (x,(lower_bound X)) <= s ; :: thesis:

end;

now :: thesis:

per cases by XXREAL_0:15;

suppose min (x,(lower_bound X)) = x ; :: thesis:

hence min (x,(lower_bound X)) in R by A2; :: thesis:

end;

suppose min (x,(lower_bound X)) = lower_bound X ; :: thesis:

hence min (x,(lower_bound X)) in R by A11, XBOOLE_0:def 5; :: thesis:

end;

end;

end;

hence lower_bound R in R by A18, A12, Def2; :: thesis:

end;

end;

end;

hence ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R ) ; :: thesis: