theorem :: WAYBEL_1:48

for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel