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