let L be non empty Poset; 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; ( f is closure implies [(inclusion f),(corestr f)] is Galois )
assume that
A1:
( f is idempotent & f is monotone )
and
A2:
id L <= f
; WAYBEL_1:def 13,WAYBEL_1:def 14 [(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; verum