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:12;
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 FUNCT_1:18 ;
:: 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)
A6: inclusion c preserves_sup_of X by A4, A5;
ex_sup_of X, Image c by YELLOW_0:17;
then sup ((inclusion c) .: X) = (inclusion c) . (sup X) by A6
.= sup X by FUNCT_1:18 ;
then sup ((inclusion c) .: X) in the carrier of (Image c) ;
hence "\/" (X,L) in the carrier of (Image c) by WAYBEL15:12; :: thesis: verum