theorem :: LATTAD_1:40

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