let L be complete LATTICE; 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; ( 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 Th18;
assume A7:
for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
"\/" (X,L) in the carrier of S
; WAYBEL_0:def 4 closure_op S is directed-sups-preserving
let X be Subset of L; WAYBEL_0:def 37 ( 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 )
; 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:111;
assume
ex_sup_of X,L
; WAYBEL_0:def 31 ( 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; "\/" (((closure_op S) .: X),L) = (closure_op S) . ("\/" (X,L))
(closure_op S) .: X is_<=_than (closure_op S) . (sup X)
then A12:
sup ((closure_op S) .: X) <= (closure_op S) . (sup X)
by YELLOW_0:32;
X is_<=_than sup ((closure_op S) .: X)
then A14:
sup X <= sup ((closure_op S) .: 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 (closure_op S) .: X
by FUNCT_2:35;
Y is directed
by A8, Th23, YELLOW_2:15;
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:10;
then
(closure_op S) . (sup ((closure_op S) .: X)) = sup ((closure_op S) .: X)
by YELLOW_2:18;
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:2; verum