let n be Element of 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 A2: ( R <> {} & card R = n + 1 ) ; :: thesis: ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )

now

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

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

then consider x being set such that
A3: R = {x} by A2, CARD_2:60;
x in R by A3, TARSKI:def 1;
then reconsider r = x as Real ;
thus R is bounded_above ; :: thesis: ( upper_bound R in R & R is bounded_below & lower_bound R in R )
upper_bound R = r by A3, SEQ_4:22;
hence upper_bound R in R by A3, 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 A3, SEQ_4:22;
hence lower_bound R in R by A3, TARSKI:def 1; :: thesis: verum

end;

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

consider x being Element of R;
reconsider x = x as Real by A2, TARSKI:def 3;
reconsider X = R \ {x} as finite Subset of REAL ;
{x} c= R by A2, ZFMISC_1:37;
then card (R \ {x}) = (card R) - (card {x}) by CARD_2:63;
then card X = (n + 1) - 1 by A2, CARD_1:50
.= n ;
then A6: ( X is bounded_above & upper_bound X in X & X is bounded_below & lower_bound X in X ) by A1, A5, CARD_1:47;
set u = upper_bound X;
set m = max x,(upper_bound X);
set l = lower_bound X;
set mi = min x,(lower_bound X);
A7: ( x <= max x,(upper_bound X) & upper_bound X <= max x,(upper_bound X) & min x,(lower_bound X) <= x & min x,(lower_bound X) <= lower_bound X ) by XXREAL_0:17, XXREAL_0:25;

A8: now

let s be real number ; :: thesis: ( s in R implies s <= max x,(upper_bound X) )
assume A9: s in R ; :: thesis: s <= max x,(upper_bound X)

now

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 A9, XBOOLE_0:def 5;
then s <= upper_bound X by SEQ_4:def 4;
hence s <= max x,(upper_bound X) by A7, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

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

A11: now

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

now

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 A12, XREAL_1:46; :: 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 A6, XBOOLE_0:def 5; :: thesis: (max x,(upper_bound X)) - r < s
thus (max x,(upper_bound X)) - r < s by A12, XREAL_1:46; :: thesis: verum

end;

end;

end;

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

end;

now

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 A6, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence upper_bound R in R by A8, A11, SEQ_4:def 4; :: thesis: ( R is bounded_below & lower_bound R in R )

A13: now

let s be real number ; :: thesis: ( s in R implies min x,(lower_bound X) <= s )
assume A14: s in R ; :: thesis: min x,(lower_bound X) <= s

now

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 A14, XBOOLE_0:def 5;
then lower_bound X <= s by SEQ_4:def 5;
hence min x,(lower_bound X) <= s by A7, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

thus R is bounded_below ; :: thesis: lower_bound R in R

A16: now

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

now

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 A17, XREAL_1:31; :: 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 A6, XBOOLE_0:def 5; :: thesis: s < (min x,(lower_bound X)) + r
thus s < (min x,(lower_bound X)) + r by A17, XREAL_1:31; :: thesis: verum

end;

end;

end;

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

end;

now

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 A6, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence lower_bound R in R by A13, A16, SEQ_4:def 5; :: 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