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 ABCA*

Proof

Step Hyp Ref Expression
1 iccssxr BC*
2 1 sseli ABCA*