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