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 Th18;

"\/" (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:111;

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)

X is_<=_than sup ((closure_op S) .: X)

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; :: thesis: verum

( 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 Th18;

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

assume A7:
for X being directed Subset of S st X <> {} & ex_sup_of X,L holds set Lk = { k where k is Element of L : (closure_op S) . k <= k } ;

set k = the Element of L;

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

then A3: (closure_op S) . the Element of L 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:52;

thus S is directed-sups-inheriting :: thesis: verum

end;set k = the Element of L;

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

proof

(closure_op S) . ((closure_op S) . the Element of L) = (closure_op S) . the Element of L
by YELLOW_2:18;
let x be object ; :: 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;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

then A3: (closure_op S) . the Element of L 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:52;

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; :: thesis: verum

end;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; :: thesis: verum

"\/" (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:111;

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

then A12:
sup ((closure_op S) .: X) <= (closure_op S) . (sup X)
by YELLOW_0:32;
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 object such that

A9: a in the carrier of L and

A10: a in X and

A11: x = (closure_op S) . a by FUNCT_2:64;

reconsider a = a as Element of L by A9;

a <= sup X by A10, YELLOW_2:22;

hence x <= (closure_op S) . (sup X) by A11, WAYBEL_1:def 2; :: thesis: verum

end;assume x in (closure_op S) .: X ; :: thesis: x <= (closure_op S) . (sup X)

then consider a being object such that

A9: a in the carrier of L and

A10: a in X and

A11: x = (closure_op S) . a by FUNCT_2:64;

reconsider a = a as Element of L by A9;

a <= sup X by A10, YELLOW_2:22;

hence x <= (closure_op S) . (sup X) by A11, WAYBEL_1:def 2; :: thesis: verum

X is_<=_than sup ((closure_op S) .: X)

proof

then A14:
sup X <= sup ((closure_op S) .: X)
by YELLOW_0:32;
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:35;

then A13: (closure_op S) . x <= sup ((closure_op S) .: X) by YELLOW_2:22;

x <= (closure_op S) . x by Th5;

hence x <= sup ((closure_op S) .: X) by A13, ORDERS_2:3; :: thesis: verum

end;assume x in X ; :: thesis: x <= sup ((closure_op S) .: X)

then (closure_op S) . x in (closure_op S) .: X by FUNCT_2:35;

then A13: (closure_op S) . x <= sup ((closure_op S) .: X) by YELLOW_2:22;

x <= (closure_op S) . x by Th5;

hence x <= sup ((closure_op S) .: X) by A13, ORDERS_2:3; :: thesis: verum

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; :: thesis: verum