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