for L being non empty Poset
for p being Function of L,L st p is projection holds
( { c where c is Element of L : c <= p . c } is non empty Subset of L & { k where k is Element of L : p . k <= k } is non empty Subset of L )