for C being complete Lattice
for X being set holds "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C)