Metamath Proof Explorer

Theorem iocssicc

Description: A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017)

Ref Expression
Assertion iocssicc 
|- ( A (,] B ) C_ ( A [,] B )

Proof

Step Hyp Ref Expression
1 df-ioc 
 |-  (,] = ( a e. RR* , b e. RR* |-> { x e. RR* | ( a < x /\ x <_ b ) } )
2 df-icc 
 |-  [,] = ( a e. RR* , b e. RR* |-> { x e. RR* | ( a <_ x /\ x <_ b ) } )
3 xrltle 
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A < w -> A <_ w ) )
4 idd 
 |-  ( ( w e. RR* /\ B e. RR* ) -> ( w <_ B -> w <_ B ) )
5 1 2 3 4 ixxssixx 
 |-  ( A (,] B ) C_ ( A [,] B )