let L be GAD_Lattice; :: thesis: for x, y being Element of L st x [= y "\/" x holds
x "\/" y = y "\/" x
let x, y be Element of L; :: thesis: ( x [= y "\/" x implies x "\/" y = y "\/" x )
assume A1: x [= y "\/" x ; :: thesis: x "\/" y = y "\/" x
x "/\" (y "\/" x) = x by LATTICES:4, A1;
hence x "\/" y = y "\/" x by Th3726; :: thesis: verum