for S being non empty 1-sorted
for T being complete LATTICE
for f, g, h being Function of S,T
for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds
h . i = sup {(f . i),(g . i)}