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

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 set such that
A5: R = {x} by A3, A4, CARD_2:60;
x in R by A5, TARSKI:def 1;
then reconsider r = x as Real ;
upper_bound R = r by A5, SEQ_4:22;
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, SEQ_4:22;
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 )

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 ;
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:37;
then card (R \ {x}) = (card R) - (card {x}) by CARD_2:63;
then A7: card X = (n + 1) - 1 by A3, CARD_1:50
.= n ;
then A8: upper_bound X in X by A1, A6, CARD_1:47;

A9: now

reconsider s = max x,(upper_bound X) as real number ;
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 A10: 0 < r ; :: thesis: ex s being real number 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

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: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 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:46; :: 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:47;

A12: now

reconsider s = min x,(lower_bound X) as real number ;
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 A13: 0 < r ; :: thesis: ex s being real number 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

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: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 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:31; :: 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

let s be real number ; :: thesis: ( s in R implies s <= max x,(upper_bound X) )
assume A16: 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 A16, XBOOLE_0:def 5;
then s <= upper_bound X by SEQ_4:def 4;
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

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, SEQ_4:def 4; :: 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

let s be real number ; :: thesis: ( s in R implies min x,(lower_bound X) <= s )
assume A19: 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 A19, XBOOLE_0:def 5;
then lower_bound X <= s by SEQ_4:def 5;
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

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, 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