Theorem odulat

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

	Ref	Expression
Hypothesis	odulat.d	⊢ 𝐷 = ( ODual ‘ 𝑂 )
Assertion	odulat	⊢ ( 𝑂 ∈ Lat → 𝐷 ∈ Lat )

Proof

Step	Hyp	Ref	Expression
1		odulat.d	⊢ 𝐷 = ( ODual ‘ 𝑂 )
2	1	odulatb	⊢ ( 𝑂 ∈ Lat → ( 𝑂 ∈ Lat ↔ 𝐷 ∈ Lat ) )
3	2	ibi	⊢ ( 𝑂 ∈ Lat → 𝐷 ∈ Lat )