Theorem odulat

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

	Ref	Expression
Hypothesis	odulat.d	|- D = ( ODual ` O )
Assertion	odulat	|- ( O e. Lat -> D e. Lat )

Proof

Step	Hyp	Ref	Expression
1		odulat.d	|- D = ( ODual ` O )
2	1	odulatb	|- ( O e. Lat -> ( O e. Lat <-> D e. Lat ) )
3	2	ibi	|- ( O e. Lat -> D e. Lat )