for L being Lattice holds
( L is D_Lattice iff L .: is D_Lattice ) by Th22, Th23;