let L be non empty join-associative meet-commutative meet-absorbing join-absorbing LattStr ; :: thesis: for a, b being Element of L holds a [= a "\/" b
let a, b be Element of L; :: thesis: a [= a "\/" b
thus a "\/" (a "\/" b) = (a "\/" a) "\/" b by Def5
.= a "\/" b ; :: according to LATTICES:def 3 :: thesis: verum