theorem Th20: :: LATTICE2:20

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