let L be non empty Poset; :: thesis: for f being Function of L,L st f is monotone & ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g ) holds
f is kernel
let f be Function of L,L; :: thesis: ( f is monotone & ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g ) implies f is kernel )
assume A1: f is monotone ; :: thesis: ( for T being non empty Poset
for g being Function of L,T
for d being Function of T,L holds
( not [g,d] is Galois or not f = d * g ) or f is kernel )
given T being non empty Poset, g being Function of L,T, d being Function of T,L such that A2: [g,d] is Galois and
A3: f = d * g ; :: thesis: f is kernel
A4: ( d is monotone & g is monotone ) by A2, Th8;
( d * g <= id L & id T <= g * d ) by A2, Th18;
then d = (d * g) * d by A4, Th20;
hence ( f is idempotent & f is monotone ) by A1, A3, Th21; :: according to WAYBEL_1:def 13,WAYBEL_1:def 15 :: thesis: f <= id L
thus f <= id L by A2, A3, Th18; :: thesis: verum