theorem Th22: :: LATTICE2:22

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