theorem Th15: :: WAYBEL_5:15

for L being complete LATTICE
for a being Element of L
for F being Function-yielding Function st ( for f being Function st f in dom (Frege F) holds
//\ (((Frege F) . f),L) <= a ) holds
Sup <= a