let L be GAD_Lattice; :: thesis: for x, y being Element of L st ex_lub_of x,y & x "\/" y = lub (x,y) holds
x "\/" y = y "\/" x
let x, y be Element of L; :: thesis: ( ex_lub_of x,y & x "\/" y = lub (x,y) implies x "\/" y = y "\/" x )
assume ( ex_lub_of x,y & x "\/" y = lub (x,y) ) ; :: thesis: x "\/" y = y "\/" x
then y [= x "\/" y by DefLUB;
then y "/\" (x "\/" y) = y by LATTICES:def 9;
hence x "\/" y = y "\/" x by Th3726; :: thesis: verum