let L be non empty Poset; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: f is closure
A4: ( d * g <= id S & id L <= g * d ) by A2, Th19;
( d is monotone & g is monotone ) by A2, Th9;
then ( d = (d * g) * d & g = (g * d) * g ) by A4, Th21;
hence ( f is idempotent & f is monotone ) by A1, A3, Th22; :: according to WAYBEL_1:def 13,WAYBEL_1:def 14 :: thesis: id L <= f
thus id L <= f by A2, A3, Th19; :: thesis: verum