for L being GAD_Lattice
for x, y being Element of L st x "/\" y = y holds
x "\/" y = x by ThA4;