for L being GAD_Lattice
for x, y being Element of L st x "/\" y [= x holds
ex z being Element of L st
( z [= x & z [= y ) by LemB1;