let L be complete LATTICE; :: thesis: for S being closure System of L holds
( closure_op S is directed-sups-preserving iff S is directed-sups-inheriting )
let S be closure System of L; :: thesis: ( closure_op S is directed-sups-preserving iff S is directed-sups-inheriting )
set c = closure_op S;
A1: Image (closure_op S) = RelStr(# the carrier of S,the InternalRel of S #) by Th19;

hereby :: thesis: ( S is directed-sups-inheriting implies closure_op S is directed-sups-preserving )

set Lk = { k where k is Element of L : (closure_op S) . k <= k } ;
consider k being Element of L;
A2: { k where k is Element of L : (closure_op S) . k <= k } c= the carrier of L

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of L : (closure_op S) . k <= k } or x in the carrier of L )
assume x in { k where k is Element of L : (closure_op S) . k <= k } ; :: thesis: x in the carrier of L
then ex k being Element of L st
( x = k & (closure_op S) . k <= k ) ;
hence x in the carrier of L ; :: thesis: verum

end;

(closure_op S) . ((closure_op S) . k) = (closure_op S) . k by YELLOW_2:20;
then A3: (closure_op S) . k in { k where k is Element of L : (closure_op S) . k <= k } ;
assume closure_op S is directed-sups-preserving ; :: thesis: S is directed-sups-inheriting
then A4: Image (closure_op S) is directed-sups-inheriting by A3, A2, WAYBEL_1:55;
thus S is directed-sups-inheriting :: thesis: verum

proof

let X be directed Subset of S; :: according to WAYBEL_0:def 4 :: thesis: ( X = {} or not ex_sup_of X,L or "\/" X,L in the carrier of S )
assume that
A5: X <> {} and
A6: ex_sup_of X,L ; :: thesis: "\/" X,L in the carrier of S
reconsider Y = X as Subset of (Image (closure_op S)) by A1;
Y is directed by A1, WAYBEL_0:3;
hence "\/" X,L in the carrier of S by A1, A4, A5, A6, WAYBEL_0:def 4; :: thesis: verum

end;

end;

assume A7: for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
"\/" X,L in the carrier of S ; :: according to WAYBEL_0:def 4 :: thesis: closure_op S is directed-sups-preserving
let X be Subset of L; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or closure_op S preserves_sup_of X )
assume A8: ( not X is empty & X is directed ) ; :: thesis: closure_op S preserves_sup_of X
rng (closure_op S) = the carrier of S by A1, YELLOW_0:def 15;
then reconsider Y = (closure_op S) .: X as Subset of S by RELAT_1:144;
assume ex_sup_of X,L ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (closure_op S) .: X,L & "\/" ((closure_op S) .: X),L = (closure_op S) . ("\/" X,L) )
thus ex_sup_of (closure_op S) .: X,L by YELLOW_0:17; :: thesis: "\/" ((closure_op S) .: X),L = (closure_op S) . ("\/" X,L)
(closure_op S) .: X is_<=_than (closure_op S) . (sup X)

proof

let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in (closure_op S) .: X or x <= (closure_op S) . (sup X) )
assume x in (closure_op S) .: X ; :: thesis: x <= (closure_op S) . (sup X)
then consider a being set such that
A9: a in the carrier of L and
A10: a in X and
A11: x = (closure_op S) . a by FUNCT_2:115;
reconsider a = a as Element of L by A9;
a <= sup X by A10, YELLOW_2:24;
hence x <= (closure_op S) . (sup X) by A11, WAYBEL_1:def 2; :: thesis: verum

end;

then A12: sup ((closure_op S) .: X) <= (closure_op S) . (sup X) by YELLOW_0:32;
X is_<=_than sup ((closure_op S) .: X)

proof

let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= sup ((closure_op S) .: X) )
assume x in X ; :: thesis: x <= sup ((closure_op S) .: X)
then (closure_op S) . x in (closure_op S) .: X by FUNCT_2:43;
then A13: (closure_op S) . x <= sup ((closure_op S) .: X) by YELLOW_2:24;
x <= (closure_op S) . x by Th6;
hence x <= sup ((closure_op S) .: X) by A13, ORDERS_2:26; :: thesis: verum

end;

then A14: sup X <= sup ((closure_op S) .: X) by YELLOW_0:32;
consider x being Element of X;
x in X by A8;
then A15: (closure_op S) . x in (closure_op S) .: X by FUNCT_2:43;
Y is directed by A8, Th24, YELLOW_2:17;
then sup ((closure_op S) .: X) in the carrier of S by A7, A15, YELLOW_0:17;
then ex a being Element of L st (closure_op S) . a = sup ((closure_op S) .: X) by A1, YELLOW_2:12;
then (closure_op S) . (sup ((closure_op S) .: X)) = sup ((closure_op S) .: X) by YELLOW_2:20;
then (closure_op S) . (sup X) <= sup ((closure_op S) .: X) by A14, WAYBEL_1:def 2;
hence "\/" ((closure_op S) .: X),L = (closure_op S) . ("\/" X,L) by A12, ORDERS_2:25; :: thesis: verum