theorem Th4: :: LATTICES:6

for L being non empty meet-commutative meet-absorbing LattStr
for a, b being Element of L holds a "/\" b [= a by Def8;