theorem :: LATTICE2:24

for L being Lattice st the L_meet of L is_distributive_wrt the L_join of L holds
L is distributive by BINOP_1:12;