let L be Quasi-Boolean_Algebra; :: thesis: for x, y being Element of L holds x "\/" (x "\/" y) = x "\/" y
let x, y be Element of L; :: thesis: x "\/" (x "\/" y) = x "\/" y
thus x "\/" (x "\/" y) = (x "\/" x) "\/" y by LATTICES:def 5
.= x "\/" y ; :: thesis: verum