theorem Th38: :: WAYBEL_1:38

for L being 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