for L being complete LATTICE
for a being Element of L
for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds F . j <= a ) holds
Sup <= a