theorem Th25: :: LATTICE2:25

for L being Lattice holds the L_meet of L is_distributive_wrt the L_meet of L