theorem :: WAYBEL_1:34

for L being non empty Poset
for f being Function of L,L st f is projection holds
ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is one-to-one & f = i * q & id T = q * i )