theorem Th28: :: WAYBEL_1:28

for L being non empty Poset
for c being Function of L,L
for X being Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds
inf X = c . (inf X)