theorem Th23: :: LATTICE2:23

for L being Lattice st L is D_Lattice holds
the L_meet of L is_distributive_wrt the L_join of L