let X be real-membered set ; :: thesis: ( X is finite implies X is real-bounded )
assume A1: X is finite ; :: thesis: X is real-bounded
per cases ( X is empty or not X is empty ) ;
suppose A2: X is empty ; :: thesis: X is real-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 ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( x in X implies 0 <= x )
thus ( x in X implies 0 <= x ) by A2; :: thesis: verum
end;
take 0 ; :: according to XXREAL_2:def 10 :: thesis: 0 is UpperBound of X
let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= 0 )
thus ( x in X implies x <= 0 ) by A2; :: thesis: verum
end;
suppose not X is empty ; :: thesis: X is real-bounded
then reconsider Y = X as real-membered finite non empty set by A1;
inf Y in X by Def5;
then reconsider m = inf X as Real ;
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 ExtReal; :: 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 ;
take m ; :: according to XXREAL_2:def 10 :: thesis: m is UpperBound of X
let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= m )
assume x in X ; :: thesis: x <= m
hence x <= m by Th4; :: thesis: verum
end;
end;