let L be complete LATTICE; :: thesis: for h being closure Function of L,L holds
( h is directed-sups-preserving iff Image h is directed-sups-inheriting )
let h be closure Function of L,L; :: thesis: ( h is directed-sups-preserving iff Image h is directed-sups-inheriting )
closure_op (Image h) = h by Th19;
hence ( h is directed-sups-preserving iff Image h is directed-sups-inheriting ) by Th24; :: thesis: verum