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 Th35, Th36;
then LowerAdj (inclusion c) is waybelow-preserving by Th22;
hence corestr c is waybelow-preserving by Th35; :: thesis: verum