let L be complete LATTICE; :: thesis: for c being closure Function of L,L st Image c is directed-sups-inheriting holds
corestr c is waybelow-preserving
let c be closure Function of L,L; :: thesis: ( Image c is directed-sups-inheriting implies corestr c is waybelow-preserving )
assume Image c is directed-sups-inheriting ; :: thesis: corestr c is waybelow-preserving
then ( inclusion c is directed-sups-preserving & inclusion c is infs-preserving ) by Th39, Th40;
then LowerAdj (inclusion c) is waybelow-preserving by Th24;
hence corestr c is waybelow-preserving by Th39; :: thesis: verum