theorem :: LATTAD_1:42

for L being GAD_Lattice
for x, y being Element of L holds
( x "\/" y = y "\/" x iff x [= y "\/" x ) by LemX3, Th3851;