Metamath Proof Explorer

Theorem ioossicc

Description: An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007)

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

Proof

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