let L be complete LATTICE; :: thesis: for c being closure Function of L,L holds
( Image c is directed-sups-inheriting iff inclusion c is directed-sups-preserving )
let c be closure Function of L,L; :: thesis: ( Image c is directed-sups-inheriting iff inclusion c is directed-sups-preserving )
set ic = inclusion c;
thus ( Image c is directed-sups-inheriting implies inclusion c is directed-sups-preserving ) :: thesis: ( inclusion c is directed-sups-preserving implies Image c is directed-sups-inheriting )

proof

assume A1: Image c is directed-sups-inheriting ; :: thesis: inclusion c is directed-sups-preserving
let D be Subset of (Image c); :: according to WAYBEL_0:def 37 :: thesis: ( D is empty or not D is directed or inclusion c preserves_sup_of D )
assume A2: ( not D is empty & D is directed ) ; :: thesis: inclusion c preserves_sup_of D
then reconsider E = D as non empty directed Subset of L by YELLOW_2:7;
A3: (inclusion c) .: D = E by WAYBEL15:14;
assume ex_sup_of D, Image c ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (inclusion c) .: D,L & "\/" ((inclusion c) .: D),L = (inclusion c) . ("\/" D,(Image c)) )
thus ex_sup_of (inclusion c) .: D,L by YELLOW_0:17; :: thesis: "\/" ((inclusion c) .: D),L = (inclusion c) . ("\/" D,(Image c))
hence sup ((inclusion c) .: D) = sup D by A1, A2, A3, WAYBEL_0:7
.= (inclusion c) . (sup D) by TMAP_1:91 ;
:: thesis: verum

end;

assume A4: inclusion c is directed-sups-preserving ; :: thesis: Image c is directed-sups-inheriting
let X be directed Subset of (Image c); :: according to WAYBEL_0:def 4 :: thesis: ( X = {} or not ex_sup_of X,L or "\/" X,L in the carrier of (Image c) )
assume A5: X <> {} ; :: thesis: ( not ex_sup_of X,L or "\/" X,L in the carrier of (Image c) )
assume ex_sup_of X,L ; :: thesis: "\/" X,L in the carrier of (Image c)
( inclusion c preserves_sup_of X & ex_sup_of X, Image c ) by A4, A5, WAYBEL_0:def 37, YELLOW_0:17;
then sup ((inclusion c) .: X) = (inclusion c) . (sup X) by WAYBEL_0:def 31
.= sup X by TMAP_1:91 ;
then sup ((inclusion c) .: X) in the carrier of (Image c) ;
hence "\/" X,L in the carrier of (Image c) by WAYBEL15:14; :: thesis: verum