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;
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 } ;
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
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;
(closure_op S) . ((closure_op S) . the Element of L) = (closure_op S) . 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 : (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;
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: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
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;
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: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;
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; :: thesis: verum