theorem :: LATTAD_1:17

for L being AD_Lattice
for x, y being Element of L st x [= y holds
x "\/" y = y "\/" x