theorem Th2: :: LATTICES:4
for L being non empty meet-absorbing join-absorbing LattStr
for a, b being Element of L holds
( a [= b iff a "/\" b = a ) by Def8, Def9;