theorem Th47: :: WAYBEL_1:47

for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure