let X be real-membered set ; :: thesis: ( X is finite implies X is bounded )
assume Z: X is finite ; :: thesis: X is bounded

per cases ( X is empty or not X is empty ) ;

suppose Z: X is empty ; :: thesis: X is bounded

thus X is bounded_below :: according to XXREAL_2:def 11 :: thesis: X is bounded_above

proof

take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of X
let x be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( x in X implies 0 <= x )
thus ( x in X implies 0 <= x ) by Z; :: thesis: verum

end;

take 0 ; :: according to XXREAL_2:def 10 :: thesis: 0 is UpperBound of X
let x be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= 0 )
thus ( x in X implies x <= 0 ) by Z; :: thesis: verum

end;

suppose not X is empty ; :: thesis: X is bounded

then reconsider Y = X as real-membered non empty finite set by Z;
inf Y in X by Def5;
then reconsider m = inf X as real number ;
thus X is bounded_below :: according to XXREAL_2:def 11 :: thesis: X is bounded_above

proof

take m ; :: according to XXREAL_2:def 9 :: thesis: m is LowerBound of X
let x be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( x in X implies m <= x )
assume x in X ; :: thesis: m <= x
hence m <= x by Th3; :: thesis: verum

end;

sup Y in X by Def6;
then reconsider m = sup X as real number ;
take m ; :: according to XXREAL_2:def 10 :: thesis: m is UpperBound of X
let x be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= m )
assume x in X ; :: thesis: x <= m
hence x <= m by Th3B; :: thesis: verum

end;

end;