Theorem suprclii

Description: Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Sep-1999)

	Ref	Expression
Hypothesis	sup3i.1	|- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x )
Assertion	suprclii	|- sup ( A , RR , < ) e. RR

Proof

Step	Hyp	Ref	Expression
1		sup3i.1	|- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x )
2		suprcl	|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
3	1 2	ax-mp	|- sup ( A , RR , < ) e. RR