let L be non empty Poset; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: according to WAYBEL_1:def 13 :: thesis: f is monotone
thus f is monotone by A1, A2, YELLOW_2:12; :: thesis: verum