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