Metamath Proof Explorer


Theorem eliccxr

Description: A member of a closed interval is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion eliccxr A B C A *

Proof

Step Hyp Ref Expression
1 iccssxr B C *
2 1 sseli A B C A *