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 ABAB

Proof

Step Hyp Ref Expression
1 df-ioo .=x*,y*z*|x<zz<y
2 df-icc .=x*,y*z*|xzzy
3 xrltle A*w*A<wAw
4 xrltle w*B*w<BwB
5 1 2 3 4 ixxssixx ABAB