let L be non empty Poset; for f being Function of L,L st f is monotone & ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d ) holds
f is closure
let f be Function of L,L; ( f is monotone & ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d ) implies f is closure )
assume A1:
f is monotone
; ( for S being non empty Poset
for g being Function of S,L
for d being Function of L,S holds
( not [g,d] is Galois or not f = g * d ) or f is closure )
given S being non empty Poset, g being Function of S,L, d being Function of L,S such that A2:
[g,d] is Galois
and
A3:
f = g * d
; f is closure
A4:
( d is monotone & g is monotone )
by A2, Th8;
( d * g <= id S & id L <= g * d )
by A2, Th18;
then
g = (g * d) * g
by A4, Th20;
hence
( f is idempotent & f is monotone )
by A1, A3, Th21; WAYBEL_1:def 13,WAYBEL_1:def 14 id L <= f
thus
id L <= f
by A2, A3, Th18; verum