Metamath Proof Explorer


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 )