let L be non empty Poset; for f being Function of L,L st ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & i is monotone & f = i * q & id T = q * i ) holds
f is projection
let f be Function of L,L; ( ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & i is monotone & f = i * q & id T = q * i ) implies f is projection )
given T being non empty Poset, q being Function of L,T, i being Function of T,L such that A1:
( q is monotone & i is monotone )
and
A2:
f = i * q
and
A3:
id T = q * i
; f is projection
(i * q) * i =
i * (id the carrier of T)
by A3, RELAT_1:36
.=
i
by FUNCT_2:17
;
hence
f is idempotent
by A2, Th21; WAYBEL_1:def 13 f is monotone
thus
f is monotone
by A1, A2, YELLOW_2:12; verum