theorem Th1: :: FILTER_0:1

for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr
for p, q, r being Element of L st p [= q holds
r "\/" p [= r "\/" q