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
A2: LowerAdj (inclusion c) = corestr c by Th35;
inclusion c is infs-preserving by Th35;
then inclusion c is directed-sups-preserving by A1, A2, Th23;
hence Image c is directed-sups-inheriting by Th36; :: thesis: verum