Metamath Proof Explorer


Theorem iccssxr

Description: A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008) (Revised by Mario Carneiro, 4-Jul-2014)

Ref Expression
Assertion iccssxr
|- ( A [,] B ) C_ RR*

Proof

Step Hyp Ref Expression
1 df-icc
 |-  [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
2 1 ixxssxr
 |-  ( A [,] B ) C_ RR*