theorem Th29: :: WAYBEL_1:29

for L being non empty Poset
for k being Function of L,L
for X being Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds
sup X = k . (sup X)