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 )

assume A2: closure_op S is directed-sups-preserving ; :: thesis: S is directed-sups-inheriting
set Lk = { k where k is Element of L : (closure_op S) . k <= k } ;
consider k being Element of L;
( (closure_op S) . ((closure_op S) . k) = (closure_op S) . k & (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 } ;
{ 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;

then A4: Image (closure_op S) is directed-sups-inheriting by A2, A3, 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 A5: ( X <> {} & 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, WAYBEL_0:def 4; :: thesis: verum

end;

end;

assume A6: 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 A7: ( not X is empty & X is directed ) ; :: thesis: closure_op S preserves_sup_of X
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 A8: ex_sup_of (closure_op S) .: X,L by YELLOW_0:17; :: thesis: "\/" ((closure_op S) .: X),L = (closure_op S) . ("\/" X,L)
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;
consider x being Element of X;
(closure_op S) .: X is directed by A7, YELLOW_2:17;
then A9: Y is directed by Th24;
( the carrier of L <> {} & x in X ) by A7;
then (closure_op S) . x in (closure_op S) .: X by FUNCT_2:43;
then sup ((closure_op S) .: X) in the carrier of S by A6, A8, A9;
then ex a being Element of L st (closure_op S) . a = sup ((closure_op S) .: X) by A1, YELLOW_2:12;
then A10: (closure_op S) . (sup ((closure_op S) .: X)) = sup ((closure_op S) .: X) by YELLOW_2:20;
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 ( x <= (closure_op S) . x & (closure_op S) . x <= sup ((closure_op S) .: X) ) by Th6, YELLOW_2:24;
hence x <= sup ((closure_op S) .: X) by ORDERS_2:26; :: thesis: verum

end;

then sup X <= sup ((closure_op S) .: X) by YELLOW_0:32;
then A11: (closure_op S) . (sup X) <= sup ((closure_op S) .: X) by A10, WAYBEL_1:def 2;
(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
A12: ( a in the carrier of L & a in X & x = (closure_op S) . a ) by FUNCT_2:115;
reconsider a = a as Element of L by A12;
a <= sup X by A12, YELLOW_2:24;
hence x <= (closure_op S) . (sup X) by A12, WAYBEL_1:def 2; :: thesis: verum

end;

then sup ((closure_op S) .: X) <= (closure_op S) . (sup X) by YELLOW_0:32;
hence "\/" ((closure_op S) .: X),L = (closure_op S) . ("\/" X,L) by A11, ORDERS_2:25; :: thesis: verum