theorem :: WAYBEL_1:52

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
( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) )