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
a "/\" (a "\/" a) = a by Def9;
hence a "/\" a = a by Th17; :: thesis: verum