let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A1: S₁[n] ; :: thesis: S₁[n + 1]
let R be finite Subset of REAL; :: thesis: ( R <> {} & card R = n + 1 implies ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R ) )
assume that
A2: R <> {} and
A3: card R = n + 1 ; :: thesis: ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )

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

per cases ( n = 0 or n <> 0 ) ;

suppose A4: n = 0 ; :: thesis: ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )

thus R is bounded_above ; :: thesis: ( upper_bound R in R & R is bounded_below & lower_bound R in R )
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: ( R is bounded_below & lower_bound R in R )
thus R is bounded_below ; :: thesis: lower_bound R in R
lower_bound R = r by A5, Th9;
hence lower_bound R in R by A5, TARSKI:def 1; :: thesis: verum

end;

suppose A6: n <> 0 ; :: thesis: ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )

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: for r being Real st 0 < r holds
ex s being Real st
( s in R & (max (x,(upper_bound X))) - r < s )

reconsider s = max (x,(upper_bound X)) as Real ;
let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( s in R & (max (x,(upper_bound X))) - r < s ) )
assume A10: 0 < r ; :: thesis: ex s being Real st
( s in R & (max (x,(upper_bound X))) - r < s )
take s = s; :: thesis: ( s in R & (max (x,(upper_bound X))) - r < s )

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

per cases ( max (x,(upper_bound X)) = x or max (x,(upper_bound X)) = upper_bound X ) by XXREAL_0:16;

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

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

end;

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

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

end;

end;

end;

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

end;

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

A12: now :: thesis: for r being Real st 0 < r holds
ex s being Real st
( s in R & s < (min (x,(lower_bound X))) + r )

reconsider s = min (x,(lower_bound X)) as Real ;
let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( s in R & s < (min (x,(lower_bound X))) + r ) )
assume A13: 0 < r ; :: thesis: ex s being Real st
( s in R & s < (min (x,(lower_bound X))) + r )
take s = s; :: thesis: ( s in R & s < (min (x,(lower_bound X))) + r )

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

per cases ( min (x,(lower_bound X)) = x or min (x,(lower_bound X)) = lower_bound X ) by XXREAL_0:15;

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

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

end;

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

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

end;

end;

end;

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

end;

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

A15: now :: thesis: for s being Real st s in R holds
s <= max (x,(upper_bound X))

let s be Real; :: thesis: ( s in R implies s <= max (x,(upper_bound X)) )
assume A16: s in R ; :: thesis: s <= max (x,(upper_bound X))

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

per cases ( s = x or s <> x ) ;

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

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

end;

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

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: verum

end;

end;

end;

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

end;

now :: thesis: max (x,(upper_bound X)) in R

per cases ( max (x,(upper_bound X)) = x or max (x,(upper_bound X)) = upper_bound X ) by XXREAL_0:16;

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

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

end;

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

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

end;

end;

end;

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

A18: now :: thesis: for s being Real st s in R holds
min (x,(lower_bound X)) <= s

let s be Real; :: thesis: ( s in R implies min (x,(lower_bound X)) <= s )
assume A19: s in R ; :: thesis: min (x,(lower_bound X)) <= s

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

per cases ( s = x or s <> x ) ;

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

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

end;

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

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: verum

end;

end;

end;

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

end;

now :: thesis: min (x,(lower_bound X)) in R

per cases ( min (x,(lower_bound X)) = x or min (x,(lower_bound X)) = lower_bound X ) by XXREAL_0:15;

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

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

end;

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

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

end;

end;

end;

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

end;

end;

end;

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