theorem Th7: :: LATTICES:9

for L being non empty meet-associative meet-absorbing join-absorbing LattStr
for a, b, c being Element of L st a [= b holds
a "/\" c [= b "/\" c