theorem :: WAYBEL_1:51

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
( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) )