let L be non empty Poset; :: thesis: for f being Function of L,L st f is closure holds
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 )
let f be Function of L,L; :: thesis: ( f is closure implies 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 ) )
assume A1: f is closure ; :: thesis: 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 )
reconsider S = Image f as non empty Poset ;
reconsider g = inclusion f as Function of S,L ;
reconsider d = corestr f as Function of L,S ;
take S ; :: thesis: ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d )
take g ; :: thesis: ex d being Function of L,S st
( [g,d] is Galois & f = g * d )
take d ; :: thesis: ( [g,d] is Galois & f = g * d )
thus [g,d] is Galois by A1, Th36; :: thesis: f = g * d
thus f = g * d by Th32; :: thesis: verum