let L be GAD_Lattice; :: thesis: for x being Element of L holds x "\/" x = x
let x be Element of L; :: thesis: x "\/" x = x
thus x "\/" x = ((x "\/" x) "/\" x) "\/" x by DefA2
.= x by LATTICES:def 8 ; :: thesis: verum