Theorem ioossioc

Description: An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	ioossioc	|- ( 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-ioc	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
3		idd	|- ( ( 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 )