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:
set c = closure_op S;
A1: Image () = RelStr(# the carrier of S, the InternalRel of S #) by Th18;
hereby :: thesis: ( S is directed-sups-inheriting implies closure_op S is directed-sups-preserving )
set Lk = { k where k is Element of L : () . k <= k } ;
set k = the Element of L;
A2: { k where k is Element of L : () . k <= k } c= the carrier of L
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of L : () . k <= k } or x in the carrier of L )
assume x in { k where k is Element of L : () . k <= k } ; :: thesis: x in the carrier of L
then ex k being Element of L st
( x = k & () . k <= k ) ;
hence x in the carrier of L ; :: thesis: verum
end;
(closure_op S) . (() . the Element of L) = () . the Element of L by YELLOW_2:18;
then A3: (closure_op S) . the Element of L in { k where k is Element of L : () . k <= k } ;
assume closure_op S is directed-sups-preserving ; :: thesis:
then A4: Image () is directed-sups-inheriting by ;
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 ()) by A1;
Y is directed by ;
hence "\/" (X,L) in the carrier of S by A1, A4, A5, A6; :: 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:
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:
rng () = the carrier of S by ;
then reconsider Y = () .: X as Subset of S by RELAT_1:111;
assume ex_sup_of X,L ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of () .: X,L & "\/" ((() .: X),L) = () . ("\/" (X,L)) )
thus ex_sup_of () .: X,L by YELLOW_0:17; :: thesis: "\/" ((() .: X),L) = () . ("\/" (X,L))
(closure_op S) .: X is_<=_than () . (sup X)
proof
let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in () .: X or x <= () . (sup X) )
assume x in () .: X ; :: thesis: x <= () . (sup X)
then consider a being object such that
A9: a in the carrier of L and
A10: a in X and
A11: x = () . a by FUNCT_2:64;
reconsider a = a as Element of L by A9;
a <= sup X by ;
hence x <= () . (sup X) by ; :: thesis: verum
end;
then A12: sup (() .: X) <= () . (sup X) by YELLOW_0:32;
X is_<=_than sup (() .: X)
proof
let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= sup (() .: X) )
assume x in X ; :: thesis: x <= sup (() .: X)
then (closure_op S) . x in () .: X by FUNCT_2:35;
then A13: (closure_op S) . x <= sup (() .: X) by YELLOW_2:22;
x <= () . x by Th5;
hence x <= sup (() .: X) by ; :: thesis: verum
end;
then A14: sup X <= sup (() .: X) by YELLOW_0:32;
set x = the Element of X;
the Element of X in X by A8;
then A15: (closure_op S) . the Element of X in () .: X by FUNCT_2:35;
Y is directed by ;
then sup (() .: X) in the carrier of S by ;
then ex a being Element of L st () . a = sup (() .: X) by ;
then (closure_op S) . (sup (() .: X)) = sup (() .: X) by YELLOW_2:18;
then (closure_op S) . (sup X) <= sup (() .: X) by ;
hence "\/" ((() .: X),L) = () . ("\/" (X,L)) by ; :: thesis: verum