theorem Th6: :: FILTER_0:6

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