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 and
A2: i is monotone and
A3: f = i * q and
A4: id T = q * i ; :: thesis: f is projection
(i * q) * i = i * (id the carrier of T) by A4, RELAT_1:55
.= i by FUNCT_2:23 ;
hence f is idempotent by A3, Th22; :: according to WAYBEL_1:def 13 :: thesis: f is monotone
thus f is monotone by A1, A2, A3, YELLOW_2:14; :: thesis: verum