for L being GAD_Lattice
for x, y being Element of L holds
( x "\/" y = y "\/" x iff ( ex_lub_of x,y & x "\/" y = lub (x,y) ) )