let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ; :: thesis: for a being Element of L holds a "\/" a = a
let a be Element of L; :: thesis: a "\/" a = a
thus a "\/" a = (a "/\" (a "\/" a)) "\/" a by Def9
.= a by Def8 ; :: thesis: verum