theorem :: LATTICE2:63

for L being D0_Lattice holds the L_meet of L is_distributive_wrt the L_join of L by Th23;