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

assume A1: X is finite ; :: thesis: X is real-bounded

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

end;

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

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

take
0
; :: according to XXREAL_2:def 10 :: thesis: 0 is UpperBound of X
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;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

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

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

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

sup Y in X
by Def6;
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;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

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