h = closure_op (Image h) by Th20;
hence Image h is directed-sups-inheriting by Th25; :: thesis: verum