theorem Th7: :: FILTER_0:7

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