let L be WA_Lattice; :: thesis: for x, y being Element of L holds x [= x "\/" y
let x, y be Element of L; :: thesis: x [= x "\/" y
set v1 = x "\/" y;
A1: x "/\" (x "\/" y) = x by LATTICES:def 9;
((x "/\" (x "\/" y)) "\/" (x "/\" (x "\/" y))) "\/" (x "\/" y) = x "\/" y by DefW33;
hence x [= x "\/" y by LATTICES:def 3, A1; :: thesis: verum