let L be non empty Poset; :: thesis: for f being Function of L,L st f is kernel holds
[(corestr f),(inclusion f)] is Galois
let f be Function of L,L; :: thesis: ( f is kernel implies [(corestr f),(inclusion f)] is Galois )
assume that
A1: ( f is idempotent & f is monotone ) and
A2: f <= id L ; :: according to WAYBEL_1:def 13,WAYBEL_1:def 15 :: thesis: [(corestr f),(inclusion f)] is Galois
set g = corestr f;
set d = inclusion f;
A3: corestr f is monotone by A1, Th33;
(corestr f) * (inclusion f) = id (Image f) by A1, Th36;
then A4: id (Image f) <= (corestr f) * (inclusion f) by Lm1;
(inclusion f) * (corestr f) <= id L by A2, Th35;
hence [(corestr f),(inclusion f)] is Galois by A3, A4, Th20; :: thesis: verum