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