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