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;
(corestr f) * (inclusion f) = id (Image f) by A1, Th33;
then A3: id (Image f) <= (corestr f) * (inclusion f) by Lm1;
( corestr f is monotone & (inclusion f) * (corestr f) <= id L ) by A1, A2, Th31, Th32;
hence [(corestr f),(inclusion f)] is Galois by A3, Th19; :: thesis: verum