Theorem odulat

Description: Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015)

	Ref	Expression
Hypothesis	odulat.d	$$⊢D=\mathrm{ODual}\left(O\right)$$
Assertion	odulat	$$⊢O\in \mathrm{Lat}\to D\in \mathrm{Lat}$$

Proof

Step	Hyp	Ref	Expression
1		odulat.d	$$⊢D=\mathrm{ODual}\left(O\right)$$
2	1	odulatb	$$⊢O\in \mathrm{Lat}\to \left(O\in \mathrm{Lat}\leftrightarrow D\in \mathrm{Lat}\right)$$
3	2	ibi	$$⊢O\in \mathrm{Lat}\to D\in \mathrm{Lat}$$