for L being non empty complete Poset
for p being Function of L,L st p is projection holds
Image p is complete