:: WAYBEL10 semantic presentation begin scheme :: WAYBEL10:sch 1 SubrelstrEx{ F1() -> non empty RelStr , P1[ set ], F2() -> set } : ex S being non empty strict full SubRelStr of F1() st for x being Element of F1() holds ( x is Element of S iff P1[x] ) provided A1: P1[F2()] and A2: F2() in the carrier of F1() proof consider A being set such that A3: for x being set holds ( x in A iff ( x in the carrier of F1() & P1[x] ) ) from XBOOLE_0:sch_1(); A c= the carrier of F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in the carrier of F1() ) thus ( not x in A or x in the carrier of F1() ) by A3; ::_thesis: verum end; then reconsider A = A as non empty Subset of F1() by A1, A2, A3; set S = subrelstr A; take subrelstr A ; ::_thesis: for x being Element of F1() holds ( x is Element of (subrelstr A) iff P1[x] ) let x be Element of F1(); ::_thesis: ( x is Element of (subrelstr A) iff P1[x] ) A4: the carrier of (subrelstr A) = A by YELLOW_0:def_15; hence ( x is Element of (subrelstr A) implies P1[x] ) by A3; ::_thesis: ( P1[x] implies x is Element of (subrelstr A) ) assume P1[x] ; ::_thesis: x is Element of (subrelstr A) hence x is Element of (subrelstr A) by A3, A4; ::_thesis: verum end; scheme :: WAYBEL10:sch 2 RelstrEq{ F1() -> non empty RelStr , F2() -> non empty RelStr , P1[ set ], P2[ set , set ] } : RelStr(# the carrier of F1(), the InternalRel of F1() #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) provided A1: for x being set holds ( x is Element of F1() iff P1[x] ) and A2: for x being set holds ( x is Element of F2() iff P1[x] ) and A3: for a, b being Element of F1() holds ( a <= b iff P2[a,b] ) and A4: for a, b being Element of F2() holds ( a <= b iff P2[a,b] ) proof set S1 = F1(); set S2 = F2(); A5: the carrier of F1() = the carrier of F2() proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of F2() c= the carrier of F1() let x be set ; ::_thesis: ( x in the carrier of F1() implies x in the carrier of F2() ) assume x in the carrier of F1() ; ::_thesis: x in the carrier of F2() then reconsider y = x as Element of F1() ; P1[y] by A1; then x is Element of F2() by A2; hence x in the carrier of F2() ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of F2() or x in the carrier of F1() ) assume x in the carrier of F2() ; ::_thesis: x in the carrier of F1() then reconsider y = x as Element of F2() ; P1[y] by A2; then x is Element of F1() by A1; hence x in the carrier of F1() ; ::_thesis: verum end; the InternalRel of F1() = the InternalRel of F2() proof let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of F1() or [x,y] in the InternalRel of F2() ) & ( not [x,y] in the InternalRel of F2() or [x,y] in the InternalRel of F1() ) ) hereby ::_thesis: ( not [x,y] in the InternalRel of F2() or [x,y] in the InternalRel of F1() ) assume A6: [x,y] in the InternalRel of F1() ; ::_thesis: [x,y] in the InternalRel of F2() then reconsider x1 = x, y1 = y as Element of F1() by ZFMISC_1:87; reconsider x2 = x1, y2 = y1 as Element of F2() by A5; x1 <= y1 by A6, ORDERS_2:def_5; then P2[x1,y1] by A3; then x2 <= y2 by A4; hence [x,y] in the InternalRel of F2() by ORDERS_2:def_5; ::_thesis: verum end; assume A7: [x,y] in the InternalRel of F2() ; ::_thesis: [x,y] in the InternalRel of F1() then reconsider x2 = x, y2 = y as Element of F2() by ZFMISC_1:87; reconsider x1 = x2, y1 = y2 as Element of F1() by A5; x2 <= y2 by A7, ORDERS_2:def_5; then P2[x2,y2] by A4; then x1 <= y1 by A3; hence [x,y] in the InternalRel of F1() by ORDERS_2:def_5; ::_thesis: verum end; hence RelStr(# the carrier of F1(), the InternalRel of F1() #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) by A5; ::_thesis: verum end; scheme :: WAYBEL10:sch 3 SubrelstrEq1{ F1() -> non empty RelStr , F2() -> non empty full SubRelStr of F1(), F3() -> non empty full SubRelStr of F1(), P1[ set ] } : RelStr(# the carrier of F2(), the InternalRel of F2() #) = RelStr(# the carrier of F3(), the InternalRel of F3() #) provided A1: for x being set holds ( x is Element of F2() iff P1[x] ) and A2: for x being set holds ( x is Element of F3() iff P1[x] ) proof A3: for x being set holds ( x is Element of F3() iff P1[x] ) by A2; defpred S1[ set , set ] means [\$1,\$2] in the InternalRel of F1(); A4: now__::_thesis:_for_a,_b_being_Element_of_F2()_holds_ (_a_<=_b_iff_S1[a,b]_) let a, b be Element of F2(); ::_thesis: ( a <= b iff S1[a,b] ) reconsider x = a, y = b as Element of F1() by YELLOW_0:58; ( x <= y iff [x,y] in the InternalRel of F1() ) by ORDERS_2:def_5; hence ( a <= b iff S1[a,b] ) by YELLOW_0:59, YELLOW_0:60; ::_thesis: verum end; A5: now__::_thesis:_for_a,_b_being_Element_of_F3()_holds_ (_a_<=_b_iff_S1[a,b]_) let a, b be Element of F3(); ::_thesis: ( a <= b iff S1[a,b] ) reconsider x = a, y = b as Element of F1() by YELLOW_0:58; ( x <= y iff [x,y] in the InternalRel of F1() ) by ORDERS_2:def_5; hence ( a <= b iff S1[a,b] ) by YELLOW_0:59, YELLOW_0:60; ::_thesis: verum end; A6: for x being set holds ( x is Element of F2() iff P1[x] ) by A1; thus RelStr(# the carrier of F2(), the InternalRel of F2() #) = RelStr(# the carrier of F3(), the InternalRel of F3() #) from WAYBEL10:sch_2(A6, A3, A4, A5); ::_thesis: verum end; scheme :: WAYBEL10:sch 4 SubrelstrEq2{ F1() -> non empty RelStr , F2() -> non empty full SubRelStr of F1(), F3() -> non empty full SubRelStr of F1(), P1[ set ] } : RelStr(# the carrier of F2(), the InternalRel of F2() #) = RelStr(# the carrier of F3(), the InternalRel of F3() #) provided A1: for x being Element of F1() holds ( x is Element of F2() iff P1[x] ) and A2: for x being Element of F1() holds ( x is Element of F3() iff P1[x] ) proof defpred S1[ set ] means ( P1[\$1] & \$1 is Element of F1() ); A3: now__::_thesis:_for_x_being_set_holds_ (_x_is_Element_of_F3()_iff_S1[x]_) let x be set ; ::_thesis: ( x is Element of F3() iff S1[x] ) ( x is Element of F3() implies x is Element of F1() ) by YELLOW_0:58; hence ( x is Element of F3() iff S1[x] ) by A2; ::_thesis: verum end; A4: now__::_thesis:_for_x_being_set_holds_ (_x_is_Element_of_F2()_iff_S1[x]_) let x be set ; ::_thesis: ( x is Element of F2() iff S1[x] ) ( x is Element of F2() implies x is Element of F1() ) by YELLOW_0:58; hence ( x is Element of F2() iff S1[x] ) by A1; ::_thesis: verum end; thus RelStr(# the carrier of F2(), the InternalRel of F2() #) = RelStr(# the carrier of F3(), the InternalRel of F3() #) from WAYBEL10:sch_3(A4, A3); ::_thesis: verum end; theorem Th1: :: WAYBEL10:1 for R, Q being Relation holds ( ( R c= Q implies R ~ c= Q ~ ) & ( R ~ c= Q ~ implies R c= Q ) & ( R ~ c= Q implies R c= Q ~ ) & ( R c= Q ~ implies R ~ c= Q ) ) proof let R, Q be Relation; ::_thesis: ( ( R c= Q implies R ~ c= Q ~ ) & ( R ~ c= Q ~ implies R c= Q ) & ( R ~ c= Q implies R c= Q ~ ) & ( R c= Q ~ implies R ~ c= Q ) ) A1: (Q ~) ~ = Q ; (R ~) ~ = R ; hence ( ( R c= Q implies R ~ c= Q ~ ) & ( R ~ c= Q ~ implies R c= Q ) & ( R ~ c= Q implies R c= Q ~ ) & ( R c= Q ~ implies R ~ c= Q ) ) by A1, SYSREL:11; ::_thesis: verum end; theorem Th2: :: WAYBEL10:2 for L, S being RelStr holds ( ( S is SubRelStr of L implies S opp is SubRelStr of L opp ) & ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) & ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) & ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) ) proof let L, S be RelStr ; ::_thesis: ( ( S is SubRelStr of L implies S opp is SubRelStr of L opp ) & ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) & ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) & ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) ) thus ( S is SubRelStr of L implies S opp is SubRelStr of L opp ) ::_thesis: ( ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) & ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) & ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) ) proof assume that A1: the carrier of S c= the carrier of L and A2: the InternalRel of S c= the InternalRel of L ; :: according to YELLOW_0:def_13 ::_thesis: S opp is SubRelStr of L opp thus ( the carrier of (S opp) c= the carrier of (L opp) & the InternalRel of (S opp) c= the InternalRel of (L opp) ) by A1, A2, Th1; :: according to YELLOW_0:def_13 ::_thesis: verum end; thus ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) ::_thesis: ( S opp is SubRelStr of L iff S is SubRelStr of L opp ) proof assume that A3: the carrier of (S opp) c= the carrier of (L opp) and A4: the InternalRel of (S opp) c= the InternalRel of (L opp) ; :: according to YELLOW_0:def_13 ::_thesis: S is SubRelStr of L thus ( the carrier of S c= the carrier of L & the InternalRel of S c= the InternalRel of L ) by A3, A4, Th1; :: according to YELLOW_0:def_13 ::_thesis: verum end; thus ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) ::_thesis: ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) proof assume that A5: the carrier of (S opp) c= the carrier of L and A6: the InternalRel of (S opp) c= the InternalRel of L ; :: according to YELLOW_0:def_13 ::_thesis: S is SubRelStr of L opp thus ( the carrier of S c= the carrier of (L opp) & the InternalRel of S c= the InternalRel of (L opp) ) by A5, A6, Th1; :: according to YELLOW_0:def_13 ::_thesis: verum end; assume that A7: the carrier of S c= the carrier of (L opp) and A8: the InternalRel of S c= the InternalRel of (L opp) ; :: according to YELLOW_0:def_13 ::_thesis: S opp is SubRelStr of L thus ( the carrier of (S opp) c= the carrier of L & the InternalRel of (S opp) c= the InternalRel of L ) by A7, A8, Th1; :: according to YELLOW_0:def_13 ::_thesis: verum end; theorem Th3: :: WAYBEL10:3 for L, S being RelStr holds ( ( S is full SubRelStr of L implies S opp is full SubRelStr of L opp ) & ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) & ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) & ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) ) proof let L, S be RelStr ; ::_thesis: ( ( S is full SubRelStr of L implies S opp is full SubRelStr of L opp ) & ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) & ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) & ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) ) A1: ( the InternalRel of L |_2 the carrier of S) ~ = ( the InternalRel of L ~) |_2 the carrier of S by ORDERS_1:83; hereby ::_thesis: ( ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) & ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) & ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) ) assume A2: S is full SubRelStr of L ; ::_thesis: S opp is full SubRelStr of L opp then the InternalRel of S = the InternalRel of L |_2 the carrier of S by YELLOW_0:def_14; hence S opp is full SubRelStr of L opp by A1, A2, Th2, YELLOW_0:def_14; ::_thesis: verum end; A3: (( the InternalRel of L ~) |_2 the carrier of S) ~ = (( the InternalRel of L ~) ~) |_2 the carrier of S by ORDERS_1:83; hereby ::_thesis: ( S opp is full SubRelStr of L iff S is full SubRelStr of L opp ) assume A4: S opp is full SubRelStr of L opp ; ::_thesis: S is full SubRelStr of L then the InternalRel of (S opp) = the InternalRel of (L opp) |_2 the carrier of S by YELLOW_0:def_14; hence S is full SubRelStr of L by A3, A4, Th2, YELLOW_0:def_14; ::_thesis: verum end; hereby ::_thesis: ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) assume A5: S opp is full SubRelStr of L ; ::_thesis: S is full SubRelStr of L opp then the InternalRel of (S opp) = the InternalRel of L |_2 the carrier of S by YELLOW_0:def_14; hence S is full SubRelStr of L opp by A1, A5, Th2, YELLOW_0:def_14; ::_thesis: verum end; assume A6: S is full SubRelStr of L opp ; ::_thesis: S opp is full SubRelStr of L then the InternalRel of S = the InternalRel of (L opp) |_2 the carrier of S by YELLOW_0:def_14; hence S opp is full SubRelStr of L by A1, A6, Th2, YELLOW_0:def_14; ::_thesis: verum end; definition let L be RelStr ; let S be full SubRelStr of L; :: original: ~ redefine funcS opp -> strict full SubRelStr of L opp ; coherence S ~ is strict full SubRelStr of L opp by Th3; end; registration let X be set ; let L be non empty RelStr ; clusterX --> L -> non-Empty ; coherence X --> L is non-Empty proof let R be 1-sorted ; :: according to WAYBEL_3:def_7 ::_thesis: ( not R in rng (X --> L) or not R is empty ) assume R in rng (X --> L) ; ::_thesis: not R is empty hence not R is empty by TARSKI:def_1; ::_thesis: verum end; end; registration let S be RelStr ; let T be non empty reflexive RelStr ; cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like V24( the carrier of S) quasi_total monotone for Element of bool [: the carrier of S, the carrier of T:]; existence ex b1 being Function of S,T st b1 is monotone proof set c = the Element of T; take f = S --> the Element of T; ::_thesis: f is monotone let x, y be Element of S; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) ) assume [x,y] in the InternalRel of S ; :: according to ORDERS_2:def_5 ::_thesis: for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) then A1: x in the carrier of S by ZFMISC_1:87; let a, b be Element of T; ::_thesis: ( not a = f . x or not b = f . y or a <= b ) assume that A2: a = f . x and A3: b = f . y ; ::_thesis: a <= b a = the Element of T by A1, A2, FUNCOP_1:7; hence a <= b by A1, A3, FUNCOP_1:7; ::_thesis: verum end; end; registration let L be non empty RelStr ; cluster Function-like quasi_total projection -> idempotent monotone for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Function of L,L st b1 is projection holds ( b1 is monotone & b1 is idempotent ) by WAYBEL_1:def_13; end; registration let S, T be non empty reflexive RelStr ; let f be monotone Function of S,T; cluster corestr f -> monotone ; coherence corestr f is monotone proof let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (corestr f) . x <= (corestr f) . y ) A1: f . y = (corestr f) . y by WAYBEL_1:30; assume x <= y ; ::_thesis: (corestr f) . x <= (corestr f) . y then A2: f . x <= f . y by WAYBEL_1:def_2; f . x = (corestr f) . x by WAYBEL_1:30; hence (corestr f) . x <= (corestr f) . y by A2, A1, YELLOW_0:60; ::_thesis: verum end; end; registration let L be non empty reflexive RelStr ; cluster id L -> infs-preserving sups-preserving ; coherence ( id L is sups-preserving & id L is infs-preserving ) proof thus id L is sups-preserving ::_thesis: id L is infs-preserving proof let X be Subset of L; :: according to WAYBEL_0:def_33 ::_thesis: id L preserves_sup_of X A1: (id L) . (sup X) = sup X by FUNCT_1:18; assume ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (id L) .: X,L & "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L)) ) hence ( ex_sup_of (id L) .: X,L & "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L)) ) by A1, FUNCT_1:92; ::_thesis: verum end; let X be Subset of L; :: according to WAYBEL_0:def_32 ::_thesis: id L preserves_inf_of X A2: (id L) . (inf X) = inf X by FUNCT_1:18; assume ex_inf_of X,L ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (id L) .: X,L & "/\" (((id L) .: X),L) = (id L) . ("/\" (X,L)) ) hence ( ex_inf_of (id L) .: X,L & "/\" (((id L) .: X),L) = (id L) . ("/\" (X,L)) ) by A2, FUNCT_1:92; ::_thesis: verum end; end; theorem :: WAYBEL10:4 for L being RelStr for S being Subset of L holds ( id S is Function of (subrelstr S),L & ( for f being Function of (subrelstr S),L st f = id S holds f is monotone ) ) proof let L be RelStr ; ::_thesis: for S being Subset of L holds ( id S is Function of (subrelstr S),L & ( for f being Function of (subrelstr S),L st f = id S holds f is monotone ) ) let S be Subset of L; ::_thesis: ( id S is Function of (subrelstr S),L & ( for f being Function of (subrelstr S),L st f = id S holds f is monotone ) ) A1: the carrier of (subrelstr S) = S by YELLOW_0:def_15; A2: rng (id S) = S by RELAT_1:45; dom (id S) = S by RELAT_1:45; hence id S is Function of (subrelstr S),L by A1, A2, FUNCT_2:2; ::_thesis: for f being Function of (subrelstr S),L st f = id S holds f is monotone let f be Function of (subrelstr S),L; ::_thesis: ( f = id S implies f is monotone ) assume A3: f = id S ; ::_thesis: f is monotone let x, y be Element of (subrelstr S); :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) ) assume A4: [x,y] in the InternalRel of (subrelstr S) ; :: according to ORDERS_2:def_5 ::_thesis: for b1, b2 being Element of the carrier of L holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) let a, b be Element of L; ::_thesis: ( not a = f . x or not b = f . y or a <= b ) assume that A5: a = f . x and A6: b = f . y ; ::_thesis: a <= b x in S by A1, A4, ZFMISC_1:87; then A7: a = x by A3, A5, FUNCT_1:17; y in S by A1, A4, ZFMISC_1:87; then A8: b = y by A3, A6, FUNCT_1:17; the InternalRel of (subrelstr S) c= the InternalRel of L by YELLOW_0:def_13; hence [a,b] in the InternalRel of L by A4, A7, A8; :: according to ORDERS_2:def_5 ::_thesis: verum end; registration let L be non empty reflexive RelStr ; cluster Relation-like the carrier of L -defined the carrier of L -valued Function-like V7() non empty V24( the carrier of L) quasi_total infs-preserving sups-preserving closure kernel for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Function of L,L st ( b1 is sups-preserving & b1 is infs-preserving & b1 is closure & b1 is kernel & b1 is V7() ) proof take id L ; ::_thesis: ( id L is sups-preserving & id L is infs-preserving & id L is closure & id L is kernel & id L is V7() ) thus ( id L is sups-preserving & id L is infs-preserving & id L is closure & id L is kernel & id L is V7() ) ; ::_thesis: verum end; end; theorem Th5: :: WAYBEL10:5 for L being non empty reflexive RelStr for c being closure Function of L,L for x being Element of L holds c . x >= x proof let L be non empty reflexive RelStr ; ::_thesis: for c being closure Function of L,L for x being Element of L holds c . x >= x let c be closure Function of L,L; ::_thesis: for x being Element of L holds c . x >= x let x be Element of L; ::_thesis: c . x >= x c >= id L by WAYBEL_1:def_14; then c . x >= (id L) . x by YELLOW_2:9; hence c . x >= x by FUNCT_1:18; ::_thesis: verum end; theorem Th6: :: WAYBEL10:6 for S, T being RelStr for R being SubRelStr of S for f being Function of the carrier of S, the carrier of T holds ( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds (f | R) . x = f . x ) ) proof let S, T be RelStr ; ::_thesis: for R being SubRelStr of S for f being Function of the carrier of S, the carrier of T holds ( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds (f | R) . x = f . x ) ) let R be SubRelStr of S; ::_thesis: for f being Function of the carrier of S, the carrier of T holds ( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds (f | R) . x = f . x ) ) let f be Function of the carrier of S, the carrier of T; ::_thesis: ( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds (f | R) . x = f . x ) ) the carrier of R c= the carrier of S by YELLOW_0:def_13; hence f | R = f | the carrier of R by TMAP_1:def_3; ::_thesis: for x being set st x in the carrier of R holds (f | R) . x = f . x hence for x being set st x in the carrier of R holds (f | R) . x = f . x by FUNCT_1:49; ::_thesis: verum end; theorem Th7: :: WAYBEL10:7 for S, T being RelStr for f being Function of S,T st f is one-to-one holds for R being SubRelStr of S holds f | R is one-to-one proof let S, T be RelStr ; ::_thesis: for f being Function of S,T st f is one-to-one holds for R being SubRelStr of S holds f | R is one-to-one let f be Function of S,T; ::_thesis: ( f is one-to-one implies for R being SubRelStr of S holds f | R is one-to-one ) assume A1: f is one-to-one ; ::_thesis: for R being SubRelStr of S holds f | R is one-to-one let R be SubRelStr of S; ::_thesis: f | R is one-to-one f | R = f | the carrier of R by Th6; hence f | R is one-to-one by A1, FUNCT_1:52; ::_thesis: verum end; registration let S, T be non empty reflexive RelStr ; let f be monotone Function of S,T; let R be SubRelStr of S; clusterf | R -> monotone ; coherence f | R is monotone proof let x, y be Element of R; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds ( not b1 = (f | R) . x or not b2 = (f | R) . y or b1 <= b2 ) ) A1: the carrier of R c= the carrier of S by YELLOW_0:def_13; assume A2: x <= y ; ::_thesis: for b1, b2 being Element of the carrier of T holds ( not b1 = (f | R) . x or not b2 = (f | R) . y or b1 <= b2 ) then A3: [x,y] in the InternalRel of R by ORDERS_2:def_5; then A4: x in the carrier of R by ZFMISC_1:87; y in the carrier of R by A3, ZFMISC_1:87; then reconsider a = x, b = y as Element of S by A4, A1; A5: a <= b by A2, YELLOW_0:59; A6: f . b = (f | R) . y by A4, Th6; f . a = (f | R) . x by A4, Th6; hence for b1, b2 being Element of the carrier of T holds ( not b1 = (f | R) . x or not b2 = (f | R) . y or b1 <= b2 ) by A5, A6, WAYBEL_1:def_2; ::_thesis: verum end; end; theorem Th8: :: WAYBEL10:8 for S, T being non empty RelStr for R being non empty SubRelStr of S for f being Function of S,T for g being Function of T,S st f is V7() & g = f " holds ( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " ) proof let S, T be non empty RelStr ; ::_thesis: for R being non empty SubRelStr of S for f being Function of S,T for g being Function of T,S st f is V7() & g = f " holds ( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " ) let R be non empty SubRelStr of S; ::_thesis: for f being Function of S,T for g being Function of T,S st f is V7() & g = f " holds ( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " ) let f be Function of S,T; ::_thesis: for g being Function of T,S st f is V7() & g = f " holds ( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " ) let g be Function of T,S; ::_thesis: ( f is V7() & g = f " implies ( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " ) ) assume that A1: f is V7() and A2: g = f " ; ::_thesis: ( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " ) set h = g | (Image (f | R)); A3: dom f = the carrier of S by FUNCT_2:def_1; A4: dom (g | (Image (f | R))) = the carrier of (Image (f | R)) by FUNCT_2:def_1; A5: the carrier of R c= the carrier of S by YELLOW_0:def_13; rng (g | (Image (f | R))) c= the carrier of R proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (g | (Image (f | R))) or y in the carrier of R ) assume y in rng (g | (Image (f | R))) ; ::_thesis: y in the carrier of R then consider x being set such that A6: x in dom (g | (Image (f | R))) and A7: y = (g | (Image (f | R))) . x by FUNCT_1:def_3; reconsider x = x as Element of (Image (f | R)) by A6; consider a being Element of R such that A8: (f | R) . a = x by YELLOW_2:10; A9: f . a = x by A8, Th6; A10: a in the carrier of R ; y = g . x by A7, Th6; hence y in the carrier of R by A1, A2, A5, A3, A10, A9, FUNCT_1:32; ::_thesis: verum end; hence g | (Image (f | R)) is Function of (Image (f | R)),R by A4, RELSET_1:4; ::_thesis: g | (Image (f | R)) = (f | R) " A11: rng (f | R) = the carrier of (Image (f | R)) by YELLOW_0:def_15; A12: f | R is V7() by A1, Th7; A13: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(Image_(f_|_R))_holds_ (g_|_(Image_(f_|_R)))_._x_=_((f_|_R)_")_._x let x be set ; ::_thesis: ( x in the carrier of (Image (f | R)) implies (g | (Image (f | R))) . x = ((f | R) ") . x ) A14: dom (f | R) = the carrier of R by FUNCT_2:def_1; assume A15: x in the carrier of (Image (f | R)) ; ::_thesis: (g | (Image (f | R))) . x = ((f | R) ") . x then consider y being set such that A16: y in dom (f | R) and A17: x = (f | R) . y by A11, FUNCT_1:def_3; A18: y = ((f | R) ") . x by A12, A16, A17, FUNCT_1:32; x = f . y by A16, A17, Th6; then y = g . x by A1, A2, A5, A3, A16, A14, FUNCT_1:32; hence (g | (Image (f | R))) . x = ((f | R) ") . x by A15, A18, Th6; ::_thesis: verum end; dom ((f | R) ") = rng (f | R) by A12, FUNCT_1:33; hence g | (Image (f | R)) = (f | R) " by A4, A11, A13, FUNCT_1:2; ::_thesis: verum end; begin registration let S be RelStr ; let T be non empty reflexive RelStr ; cluster MonMaps (S,T) -> non empty ; coherence not MonMaps (S,T) is empty proof set f = the monotone Function of S,T; the monotone Function of S,T in Funcs ( the carrier of S, the carrier of T) by FUNCT_2:8; hence not MonMaps (S,T) is empty by YELLOW_1:def_6; ::_thesis: verum end; end; theorem Th9: :: WAYBEL10:9 for S being RelStr for T being non empty reflexive RelStr for x being set holds ( x is Element of (MonMaps (S,T)) iff x is monotone Function of S,T ) proof let S be RelStr ; ::_thesis: for T being non empty reflexive RelStr for x being set holds ( x is Element of (MonMaps (S,T)) iff x is monotone Function of S,T ) let T be non empty reflexive RelStr ; ::_thesis: for x being set holds ( x is Element of (MonMaps (S,T)) iff x is monotone Function of S,T ) let x be set ; ::_thesis: ( x is Element of (MonMaps (S,T)) iff x is monotone Function of S,T ) hereby ::_thesis: ( x is monotone Function of S,T implies x is Element of (MonMaps (S,T)) ) assume x is Element of (MonMaps (S,T)) ; ::_thesis: x is monotone Function of S,T then reconsider f = x as Element of (MonMaps (S,T)) ; f is Element of (T |^ the carrier of S) by YELLOW_0:58; then f in the carrier of (T |^ the carrier of S) ; then f in Funcs ( the carrier of S, the carrier of T) by YELLOW_1:28; then reconsider f = f as Function of S,T by FUNCT_2:66; f in the carrier of (MonMaps (S,T)) ; hence x is monotone Function of S,T by YELLOW_1:def_6; ::_thesis: verum end; assume x is monotone Function of S,T ; ::_thesis: x is Element of (MonMaps (S,T)) then reconsider f = x as monotone Function of S,T ; f in Funcs ( the carrier of S, the carrier of T) by FUNCT_2:8; hence x is Element of (MonMaps (S,T)) by YELLOW_1:def_6; ::_thesis: verum end; definition let L be non empty reflexive RelStr ; func ClOpers L -> non empty strict full SubRelStr of MonMaps (L,L) means :Def1: :: WAYBEL10:def 1 for f being Function of L,L holds ( f is Element of it iff f is closure ); existence ex b1 being non empty strict full SubRelStr of MonMaps (L,L) st for f being Function of L,L holds ( f is Element of b1 iff f is closure ) proof defpred S1[ set ] means \$1 is closure Function of L,L; set h = the closure Function of L,L; the closure Function of L,L in Funcs ( the carrier of L, the carrier of L) by FUNCT_2:9; then A1: the closure Function of L,L in the carrier of (MonMaps (L,L)) by YELLOW_1:def_6; A2: S1[ the closure Function of L,L] ; consider S being non empty strict full SubRelStr of MonMaps (L,L) such that A3: for f being Element of (MonMaps (L,L)) holds ( f is Element of S iff S1[f] ) from WAYBEL10:sch_1(A2, A1); take S ; ::_thesis: for f being Function of L,L holds ( f is Element of S iff f is closure ) let f be Function of L,L; ::_thesis: ( f is Element of S iff f is closure ) hereby ::_thesis: ( f is closure implies f is Element of S ) assume A4: f is Element of S ; ::_thesis: f is closure then f is Element of (MonMaps (L,L)) by YELLOW_0:58; hence f is closure by A3, A4; ::_thesis: verum end; assume A5: f is closure ; ::_thesis: f is Element of S f in Funcs ( the carrier of L, the carrier of L) by FUNCT_2:9; then f in the carrier of (MonMaps (L,L)) by A5, YELLOW_1:def_6; hence f is Element of S by A3, A5; ::_thesis: verum end; correctness uniqueness for b1, b2 being non empty strict full SubRelStr of MonMaps (L,L) st ( for f being Function of L,L holds ( f is Element of b1 iff f is closure ) ) & ( for f being Function of L,L holds ( f is Element of b2 iff f is closure ) ) holds b1 = b2; proof let S1, S2 be non empty strict full SubRelStr of MonMaps (L,L); ::_thesis: ( ( for f being Function of L,L holds ( f is Element of S1 iff f is closure ) ) & ( for f being Function of L,L holds ( f is Element of S2 iff f is closure ) ) implies S1 = S2 ) assume that A6: for f being Function of L,L holds ( f is Element of S1 iff f is closure ) and A7: for f being Function of L,L holds ( f is Element of S2 iff f is closure ) ; ::_thesis: S1 = S2 the carrier of S1 = the carrier of S2 proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of S2 c= the carrier of S1 let x be set ; ::_thesis: ( x in the carrier of S1 implies x in the carrier of S2 ) assume x in the carrier of S1 ; ::_thesis: x in the carrier of S2 then reconsider y = x as Element of S1 ; y is Element of (MonMaps (L,L)) by YELLOW_0:58; then reconsider y = y as Function of L,L by Th9; y is closure by A6; then y is Element of S2 by A7; hence x in the carrier of S2 ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of S2 or x in the carrier of S1 ) assume x in the carrier of S2 ; ::_thesis: x in the carrier of S1 then reconsider y = x as Element of S2 ; y is Element of (MonMaps (L,L)) by YELLOW_0:58; then reconsider y = y as Function of L,L by Th9; y is closure by A7; then y is Element of S1 by A6; hence x in the carrier of S1 ; ::_thesis: verum end; hence S1 = S2 by YELLOW_0:57; ::_thesis: verum end; end; :: deftheorem Def1 defines ClOpers WAYBEL10:def_1_:_ for L being non empty reflexive RelStr for b2 being non empty strict full SubRelStr of MonMaps (L,L) holds ( b2 = ClOpers L iff for f being Function of L,L holds ( f is Element of b2 iff f is closure ) ); theorem Th10: :: WAYBEL10:10 for L being non empty reflexive RelStr for x being set holds ( x is Element of (ClOpers L) iff x is closure Function of L,L ) proof let L be non empty reflexive RelStr ; ::_thesis: for x being set holds ( x is Element of (ClOpers L) iff x is closure Function of L,L ) let x be set ; ::_thesis: ( x is Element of (ClOpers L) iff x is closure Function of L,L ) ( x is Element of (ClOpers L) implies x is Element of (MonMaps (L,L)) ) by YELLOW_0:58; hence ( x is Element of (ClOpers L) iff x is closure Function of L,L ) by Def1, Th9; ::_thesis: verum end; theorem Th11: :: WAYBEL10:11 for X being set for L being non empty RelStr for f, g being Function of X, the carrier of L for x, y being Element of (L |^ X) st x = f & y = g holds ( x <= y iff f <= g ) proof let X be set ; ::_thesis: for L being non empty RelStr for f, g being Function of X, the carrier of L for x, y being Element of (L |^ X) st x = f & y = g holds ( x <= y iff f <= g ) let L be non empty RelStr ; ::_thesis: for f, g being Function of X, the carrier of L for x, y being Element of (L |^ X) st x = f & y = g holds ( x <= y iff f <= g ) let f, g be Function of X, the carrier of L; ::_thesis: for x, y being Element of (L |^ X) st x = f & y = g holds ( x <= y iff f <= g ) let x, y be Element of (L |^ X); ::_thesis: ( x = f & y = g implies ( x <= y iff f <= g ) ) assume that A1: x = f and A2: y = g ; ::_thesis: ( x <= y iff f <= g ) set J = X --> L; A3: L |^ X = product (X --> L) by YELLOW_1:def_5; A4: the carrier of (product (X --> L)) = product (Carrier (X --> L)) by YELLOW_1:def_4; then A5: ( x <= y iff ex f, g being Function st ( f = x & g = y & ( for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = (X --> L) . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) by A3, YELLOW_1:def_4; hereby ::_thesis: ( f <= g implies x <= y ) assume A6: x <= y ; ::_thesis: f <= g thus f <= g ::_thesis: verum proof let i be set ; :: according to YELLOW_2:def_1 ::_thesis: ( not i in X or ex b1, b2 being Element of the carrier of L st ( b1 = f . i & b2 = g . i & b1 <= b2 ) ) assume A7: i in X ; ::_thesis: ex b1, b2 being Element of the carrier of L st ( b1 = f . i & b2 = g . i & b1 <= b2 ) then A8: (X --> L) . i = L by FUNCOP_1:7; ex R being RelStr ex xi, yi being Element of R st ( R = (X --> L) . i & xi = f . i & yi = g . i & xi <= yi ) by A1, A2, A5, A6, A7; hence ex b1, b2 being Element of the carrier of L st ( b1 = f . i & b2 = g . i & b1 <= b2 ) by A8; ::_thesis: verum end; end; assume A9: for j being set st j in X holds ex a, b being Element of L st ( a = f . j & b = g . j & a <= b ) ; :: according to YELLOW_2:def_1 ::_thesis: x <= y now__::_thesis:_ex_f9,_g9_being_Function_st_ (_f9_=_x_&_g9_=_y_&_(_for_i_being_set_st_i_in_X_holds_ ex_R_being_RelStr_ex_xi,_yi_being_Element_of_R_st_ (_R_=_(X_-->_L)_._i_&_xi_=_f9_._i_&_yi_=_g9_._i_&_xi_<=_yi_)_)_) reconsider f9 = f, g9 = g as Function ; take f9 = f9; ::_thesis: ex g9 being Function st ( f9 = x & g9 = y & ( for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi ) ) ) take g9 = g9; ::_thesis: ( f9 = x & g9 = y & ( for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi ) ) ) thus ( f9 = x & g9 = y ) by A1, A2; ::_thesis: for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi ) let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st ( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi ) ) assume A10: i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st ( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi ) then A11: (X --> L) . i = L by FUNCOP_1:7; ex a, b being Element of L st ( a = f . i & b = g . i & a <= b ) by A9, A10; hence ex R being RelStr ex xi, yi being Element of R st ( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi ) by A11; ::_thesis: verum end; hence x <= y by A4, A3, YELLOW_1:def_4; ::_thesis: verum end; theorem Th12: :: WAYBEL10:12 for L being complete LATTICE for c1, c2 being Function of L,L for x, y being Element of (ClOpers L) st x = c1 & y = c2 holds ( x <= y iff c1 <= c2 ) proof let L be complete LATTICE; ::_thesis: for c1, c2 being Function of L,L for x, y being Element of (ClOpers L) st x = c1 & y = c2 holds ( x <= y iff c1 <= c2 ) let c1, c2 be Function of L,L; ::_thesis: for x, y being Element of (ClOpers L) st x = c1 & y = c2 holds ( x <= y iff c1 <= c2 ) let x, y be Element of (ClOpers L); ::_thesis: ( x = c1 & y = c2 implies ( x <= y iff c1 <= c2 ) ) assume that A1: x = c1 and A2: y = c2 ; ::_thesis: ( x <= y iff c1 <= c2 ) reconsider x9 = x, y9 = y as Element of (MonMaps (L,L)) by YELLOW_0:58; reconsider x99 = x9, y99 = y9 as Element of (L |^ the carrier of L) by YELLOW_0:58; ( x99 <= y99 iff x9 <= y9 ) by YELLOW_0:59, YELLOW_0:60; hence ( x <= y iff c1 <= c2 ) by A1, A2, Th11, YELLOW_0:59, YELLOW_0:60; ::_thesis: verum end; theorem Th13: :: WAYBEL10:13 for L being reflexive RelStr for S1, S2 being full SubRelStr of L st the carrier of S1 c= the carrier of S2 holds S1 is SubRelStr of S2 proof let L be reflexive RelStr ; ::_thesis: for S1, S2 being full SubRelStr of L st the carrier of S1 c= the carrier of S2 holds S1 is SubRelStr of S2 let S1, S2 be full SubRelStr of L; ::_thesis: ( the carrier of S1 c= the carrier of S2 implies S1 is SubRelStr of S2 ) assume A1: the carrier of S1 c= the carrier of S2 ; ::_thesis: S1 is SubRelStr of S2 hence the carrier of S1 c= the carrier of S2 ; :: according to YELLOW_0:def_13 ::_thesis: the InternalRel of S1 c= the InternalRel of S2 let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the InternalRel of S1 or [x,y] in the InternalRel of S2 ) assume A2: [x,y] in the InternalRel of S1 ; ::_thesis: [x,y] in the InternalRel of S2 then A3: x in the carrier of S1 by ZFMISC_1:87; A4: y in the carrier of S1 by A2, ZFMISC_1:87; reconsider x = x, y = y as Element of S1 by A2, ZFMISC_1:87; the carrier of S1 c= the carrier of L by YELLOW_0:def_13; then reconsider a = x, b = y as Element of L by A3, A4; reconsider x9 = x, y9 = y as Element of S2 by A1, A3, A4; x <= y by A2, ORDERS_2:def_5; then a <= b by YELLOW_0:59; then x9 <= y9 by A1, A3, YELLOW_0:60; hence [x,y] in the InternalRel of S2 by ORDERS_2:def_5; ::_thesis: verum end; theorem Th14: :: WAYBEL10:14 for L being complete LATTICE for c1, c2 being closure Function of L,L holds ( c1 <= c2 iff Image c2 is SubRelStr of Image c1 ) proof let L be complete LATTICE; ::_thesis: for c1, c2 being closure Function of L,L holds ( c1 <= c2 iff Image c2 is SubRelStr of Image c1 ) let c1, c2 be closure Function of L,L; ::_thesis: ( c1 <= c2 iff Image c2 is SubRelStr of Image c1 ) hereby ::_thesis: ( Image c2 is SubRelStr of Image c1 implies c1 <= c2 ) assume A1: c1 <= c2 ; ::_thesis: Image c2 is SubRelStr of Image c1 the carrier of (Image c2) c= the carrier of (Image c1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (Image c2) or x in the carrier of (Image c1) ) assume x in the carrier of (Image c2) ; ::_thesis: x in the carrier of (Image c1) then consider y being Element of L such that A2: c2 . y = x by YELLOW_2:10; A3: c2 . (c2 . y) = c2 . y by YELLOW_2:18; A4: c1 . (c2 . y) <= c2 . (c2 . y) by A1, YELLOW_2:9; c2 . y <= c1 . (c2 . y) by Th5; then c1 . (c2 . y) = x by A2, A4, A3, ORDERS_2:2; then x in rng c1 by FUNCT_2:4; hence x in the carrier of (Image c1) by YELLOW_0:def_15; ::_thesis: verum end; hence Image c2 is SubRelStr of Image c1 by Th13; ::_thesis: verum end; assume that A5: the carrier of (Image c2) c= the carrier of (Image c1) and the InternalRel of (Image c2) c= the InternalRel of (Image c1) ; :: according to YELLOW_0:def_13 ::_thesis: c1 <= c2 now__::_thesis:_for_x_being_Element_of_L_holds_c1_._x_<=_c2_._x let x be Element of L; ::_thesis: c1 . x <= c2 . x c2 . x in rng c2 by FUNCT_2:4; then c2 . x in the carrier of (Image c2) by YELLOW_0:def_15; then ex a being Element of L st c1 . a = c2 . x by A5, YELLOW_2:10; then A6: c1 . (c2 . x) = c2 . x by YELLOW_2:18; x <= c2 . x by Th5; hence c1 . x <= c2 . x by A6, WAYBEL_1:def_2; ::_thesis: verum end; hence c1 <= c2 by YELLOW_2:9; ::_thesis: verum end; begin definition let L be RelStr ; func Sub L -> non empty strict RelStr means :Def2: :: WAYBEL10:def 2 ( ( for x being set holds ( x is Element of it iff x is strict SubRelStr of L ) ) & ( for a, b being Element of it holds ( a <= b iff ex R being RelStr st ( b = R & a is SubRelStr of R ) ) ) ); existence ex b1 being non empty strict RelStr st ( ( for x being set holds ( x is Element of b1 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b1 holds ( a <= b iff ex R being RelStr st ( b = R & a is SubRelStr of R ) ) ) ) proof set X = { RelStr(# A,B #) where A is Subset of L, B is Relation of A,A : B c= the InternalRel of L } ; A1: the InternalRel of (subrelstr ({} L)) c= the InternalRel of L by YELLOW_0:def_13; the carrier of (subrelstr ({} L)) = {} L by YELLOW_0:def_15; then subrelstr ({} L) in { RelStr(# A,B #) where A is Subset of L, B is Relation of A,A : B c= the InternalRel of L } by A1; then reconsider X = { RelStr(# A,B #) where A is Subset of L, B is Relation of A,A : B c= the InternalRel of L } as non empty set ; defpred S1[ set , set ] means ex R being RelStr st ( \$2 = R & \$1 is SubRelStr of R ); consider S being non empty strict RelStr such that A2: the carrier of S = X and A3: for a, b being Element of S holds ( a <= b iff S1[a,b] ) from YELLOW_0:sch_1(); take S ; ::_thesis: ( ( for x being set holds ( x is Element of S iff x is strict SubRelStr of L ) ) & ( for a, b being Element of S holds ( a <= b iff ex R being RelStr st ( b = R & a is SubRelStr of R ) ) ) ) hereby ::_thesis: for a, b being Element of S holds ( a <= b iff ex R being RelStr st ( b = R & a is SubRelStr of R ) ) let x be set ; ::_thesis: ( ( x is Element of S implies x is strict SubRelStr of L ) & ( x is strict SubRelStr of L implies x is Element of S ) ) hereby ::_thesis: ( x is strict SubRelStr of L implies x is Element of S ) assume x is Element of S ; ::_thesis: x is strict SubRelStr of L then x in X by A2; then ex A being Subset of L ex B being Relation of A,A st ( x = RelStr(# A,B #) & B c= the InternalRel of L ) ; hence x is strict SubRelStr of L by YELLOW_0:def_13; ::_thesis: verum end; assume x is strict SubRelStr of L ; ::_thesis: x is Element of S then reconsider R = x as strict SubRelStr of L ; A4: the InternalRel of R c= the InternalRel of L by YELLOW_0:def_13; the carrier of R c= the carrier of L by YELLOW_0:def_13; then R in X by A4; hence x is Element of S by A2; ::_thesis: verum end; thus for a, b being Element of S holds ( a <= b iff ex R being RelStr st ( b = R & a is SubRelStr of R ) ) by A3; ::_thesis: verum end; correctness uniqueness for b1, b2 being non empty strict RelStr st ( for x being set holds ( x is Element of b1 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b1 holds ( a <= b iff ex R being RelStr st ( b = R & a is SubRelStr of R ) ) ) & ( for x being set holds ( x is Element of b2 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b2 holds ( a <= b iff ex R being RelStr st ( b = R & a is SubRelStr of R ) ) ) holds b1 = b2; proof defpred S1[ set , set ] means ex R being RelStr st ( \$2 = R & \$1 is SubRelStr of R ); defpred S2[ set ] means \$1 is strict SubRelStr of L; let S1, S2 be non empty strict RelStr ; ::_thesis: ( ( for x being set holds ( x is Element of S1 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of S1 holds ( a <= b iff ex R being RelStr st ( b = R & a is SubRelStr of R ) ) ) & ( for x being set holds ( x is Element of S2 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of S2 holds ( a <= b iff ex R being RelStr st ( b = R & a is SubRelStr of R ) ) ) implies S1 = S2 ) assume that A5: for x being set holds ( x is Element of S1 iff S2[x] ) and A6: for a, b being Element of S1 holds ( a <= b iff S1[a,b] ) and A7: for x being set holds ( x is Element of S2 iff S2[x] ) and A8: for a, b being Element of S2 holds ( a <= b iff S1[a,b] ) ; ::_thesis: S1 = S2 RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) from WAYBEL10:sch_2(A5, A7, A6, A8); hence S1 = S2 ; ::_thesis: verum end; end; :: deftheorem Def2 defines Sub WAYBEL10:def_2_:_ for L being RelStr for b2 being non empty strict RelStr holds ( b2 = Sub L iff ( ( for x being set holds ( x is Element of b2 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b2 holds ( a <= b iff ex R being RelStr st ( b = R & a is SubRelStr of R ) ) ) ) ); theorem Th15: :: WAYBEL10:15 for L, R being RelStr for x, y being Element of (Sub L) st y = R holds ( x <= y iff x is SubRelStr of R ) proof let L, R be RelStr ; ::_thesis: for x, y being Element of (Sub L) st y = R holds ( x <= y iff x is SubRelStr of R ) let x, y be Element of (Sub L); ::_thesis: ( y = R implies ( x <= y iff x is SubRelStr of R ) ) ( x <= y iff ex R being RelStr st ( y = R & x is SubRelStr of R ) ) by Def2; hence ( y = R implies ( x <= y iff x is SubRelStr of R ) ) ; ::_thesis: verum end; registration let L be RelStr ; cluster Sub L -> non empty strict reflexive transitive antisymmetric ; coherence ( Sub L is reflexive & Sub L is antisymmetric & Sub L is transitive ) proof set R = Sub L; thus Sub L is reflexive ::_thesis: ( Sub L is antisymmetric & Sub L is transitive ) proof let x be Element of (Sub L); :: according to YELLOW_0:def_1 ::_thesis: x <= x reconsider A = x as strict SubRelStr of L by Def2; A is SubRelStr of A by YELLOW_0:def_13; hence x <= x by Th15; ::_thesis: verum end; thus Sub L is antisymmetric ::_thesis: Sub L is transitive proof let x, y be Element of (Sub L); :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y ) reconsider A = x, B = y as strict SubRelStr of L by Def2; assume that A1: x <= y and A2: y <= x ; ::_thesis: x = y A3: B is SubRelStr of A by A2, Th15; then A4: the carrier of B c= the carrier of A by YELLOW_0:def_13; A5: A is SubRelStr of B by A1, Th15; then the carrier of A c= the carrier of B by YELLOW_0:def_13; then A6: the carrier of A = the carrier of B by A4, XBOOLE_0:def_10; A7: the InternalRel of B c= the InternalRel of A by A3, YELLOW_0:def_13; the InternalRel of A c= the InternalRel of B by A5, YELLOW_0:def_13; hence x = y by A7, A6, XBOOLE_0:def_10; ::_thesis: verum end; thus Sub L is transitive ::_thesis: verum proof let x, y, z be Element of (Sub L); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) reconsider A = x, B = y, C = z as strict SubRelStr of L by Def2; assume that A8: x <= y and A9: y <= z ; ::_thesis: x <= z A10: B is SubRelStr of C by A9, Th15; then A11: the carrier of B c= the carrier of C by YELLOW_0:def_13; A12: the InternalRel of B c= the InternalRel of C by A10, YELLOW_0:def_13; A13: A is SubRelStr of B by A8, Th15; then the InternalRel of A c= the InternalRel of B by YELLOW_0:def_13; then A14: the InternalRel of A c= the InternalRel of C by A12, XBOOLE_1:1; the carrier of A c= the carrier of B by A13, YELLOW_0:def_13; then the carrier of A c= the carrier of C by A11, XBOOLE_1:1; then A is SubRelStr of C by A14, YELLOW_0:def_13; hence x <= z by Th15; ::_thesis: verum end; end; end; registration let L be RelStr ; cluster Sub L -> non empty strict complete ; coherence Sub L is complete proof now__::_thesis:_for_X_being_Subset_of_(Sub_L)_holds_ex_sup_of_X,_Sub_L let X be Subset of (Sub L); ::_thesis: ex_sup_of X, Sub L now__::_thesis:_ex_a_being_Element_of_(Sub_L)_st_ (_X_is_<=_than_a_&_(_for_b_being_Element_of_(Sub_L)_st_X_is_<=_than_b_holds_ a_<=_b_)_) defpred S1[ set ] means ex R being RelStr st ( R in X & L in the InternalRel of R ); defpred S2[ set ] means ex R being RelStr st ( R in X & L in the carrier of R ); consider Y being set such that A1: for x being set holds ( x in Y iff ( x in the carrier of L & S2[x] ) ) from XBOOLE_0:sch_1(); consider S being set such that A2: for x being set holds ( x in S iff ( x in the InternalRel of L & S1[x] ) ) from XBOOLE_0:sch_1(); A3: S c= [:Y,Y:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in [:Y,Y:] ) assume x in S ; ::_thesis: x in [:Y,Y:] then consider R being RelStr such that A4: R in X and A5: x in the InternalRel of R by A2; the carrier of R c= Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R or x in Y ) R is SubRelStr of L by A4, Def2; then A6: the carrier of R c= the carrier of L by YELLOW_0:def_13; assume x in the carrier of R ; ::_thesis: x in Y hence x in Y by A1, A4, A6; ::_thesis: verum end; then A7: [: the carrier of R, the carrier of R:] c= [:Y,Y:] by ZFMISC_1:96; x in [: the carrier of R, the carrier of R:] by A5; hence x in [:Y,Y:] by A7; ::_thesis: verum end; A8: S c= the InternalRel of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in the InternalRel of L ) thus ( not x in S or x in the InternalRel of L ) by A2; ::_thesis: verum end; reconsider S = S as Relation of Y by A3; Y c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in the carrier of L ) thus ( not x in Y or x in the carrier of L ) by A1; ::_thesis: verum end; then reconsider A = RelStr(# Y,S #) as SubRelStr of L by A8, YELLOW_0:def_13; reconsider a = A as Element of (Sub L) by Def2; take a = a; ::_thesis: ( X is_<=_than a & ( for b being Element of (Sub L) st X is_<=_than b holds a <= b ) ) thus X is_<=_than a ::_thesis: for b being Element of (Sub L) st X is_<=_than b holds a <= b proof let b be Element of (Sub L); :: according to LATTICE3:def_9 ::_thesis: ( not b in X or b <= a ) reconsider R = b as strict SubRelStr of L by Def2; assume A9: b in X ; ::_thesis: b <= a A10: the InternalRel of R c= S proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the InternalRel of R or [x,y] in S ) A11: the InternalRel of R c= the InternalRel of L by YELLOW_0:def_13; assume [x,y] in the InternalRel of R ; ::_thesis: [x,y] in S hence [x,y] in S by A2, A9, A11; ::_thesis: verum end; the carrier of R c= Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R or x in Y ) A12: the carrier of R c= the carrier of L by YELLOW_0:def_13; assume x in the carrier of R ; ::_thesis: x in Y hence x in Y by A1, A9, A12; ::_thesis: verum end; then R is SubRelStr of A by A10, YELLOW_0:def_13; hence b <= a by Th15; ::_thesis: verum end; let b be Element of (Sub L); ::_thesis: ( X is_<=_than b implies a <= b ) reconsider B = b as strict SubRelStr of L by Def2; assume A13: X is_<=_than b ; ::_thesis: a <= b A14: S c= the InternalRel of B proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in S or [x,y] in the InternalRel of B ) assume [x,y] in S ; ::_thesis: [x,y] in the InternalRel of B then consider R being RelStr such that A15: R in X and A16: [x,y] in the InternalRel of R by A2; reconsider c = R as Element of (Sub L) by A15; c <= b by A13, A15, LATTICE3:def_9; then R is SubRelStr of B by Th15; then the InternalRel of R c= the InternalRel of B by YELLOW_0:def_13; hence [x,y] in the InternalRel of B by A16; ::_thesis: verum end; Y c= the carrier of B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in the carrier of B ) assume x in Y ; ::_thesis: x in the carrier of B then consider R being RelStr such that A17: R in X and A18: x in the carrier of R by A1; reconsider c = R as Element of (Sub L) by A17; c <= b by A13, A17, LATTICE3:def_9; then R is SubRelStr of B by Th15; then the carrier of R c= the carrier of B by YELLOW_0:def_13; hence x in the carrier of B by A18; ::_thesis: verum end; then a is SubRelStr of B by A14, YELLOW_0:def_13; hence a <= b by Th15; ::_thesis: verum end; hence ex_sup_of X, Sub L by YELLOW_0:15; ::_thesis: verum end; hence Sub L is complete by YELLOW_0:53; ::_thesis: verum end; end; registration let L be complete LATTICE; cluster infs-inheriting -> non empty for SubRelStr of L; coherence for b1 being SubRelStr of L st b1 is infs-inheriting holds not b1 is empty proof let S be SubRelStr of L; ::_thesis: ( S is infs-inheriting implies not S is empty ) assume A1: S is infs-inheriting ; ::_thesis: not S is empty ex_inf_of {} S,L by YELLOW_0:17; hence not S is empty by A1, YELLOW_0:def_18; ::_thesis: verum end; cluster sups-inheriting -> non empty for SubRelStr of L; coherence for b1 being SubRelStr of L st b1 is sups-inheriting holds not b1 is empty proof let S be SubRelStr of L; ::_thesis: ( S is sups-inheriting implies not S is empty ) assume A2: S is sups-inheriting ; ::_thesis: not S is empty ex_sup_of {} S,L by YELLOW_0:17; hence not S is empty by A2, YELLOW_0:def_19; ::_thesis: verum end; end; definition let L be RelStr ; mode System of L is full SubRelStr of L; end; notation let L be non empty RelStr ; let S be System of L; synonym closure S for infs-inheriting ; end; registration let L be non empty RelStr ; cluster subrelstr ([#] L) -> infs-inheriting sups-inheriting ; coherence ( subrelstr ([#] L) is closure & subrelstr ([#] L) is sups-inheriting ) proof set SL = subrelstr ([#] L); A1: the carrier of (subrelstr ([#] L)) = the carrier of L by YELLOW_0:def_15; thus subrelstr ([#] L) is infs-inheriting ::_thesis: subrelstr ([#] L) is sups-inheriting proof let X be Subset of (subrelstr ([#] L)); :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (subrelstr ([#] L)) ) thus ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (subrelstr ([#] L)) ) by A1; ::_thesis: verum end; let X be Subset of (subrelstr ([#] L)); :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr ([#] L)) ) thus ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr ([#] L)) ) by A1; ::_thesis: verum end; end; definition let L be non empty RelStr ; func ClosureSystems L -> non empty strict full SubRelStr of Sub L means :Def3: :: WAYBEL10:def 3 for R being strict SubRelStr of L holds ( R is Element of it iff ( R is infs-inheriting & R is full ) ); existence ex b1 being non empty strict full SubRelStr of Sub L st for R being strict SubRelStr of L holds ( R is Element of b1 iff ( R is infs-inheriting & R is full ) ) proof defpred S1[ set ] means \$1 is full infs-inheriting SubRelStr of L; set SL = subrelstr ([#] L); subrelstr ([#] L) is Element of (Sub L) by Def2; then A1: subrelstr ([#] L) in the carrier of (Sub L) ; A2: S1[ subrelstr ([#] L)] ; consider S being non empty strict full SubRelStr of Sub L such that A3: for x being Element of (Sub L) holds ( x is Element of S iff S1[x] ) from WAYBEL10:sch_1(A2, A1); take S ; ::_thesis: for R being strict SubRelStr of L holds ( R is Element of S iff ( R is infs-inheriting & R is full ) ) let R be strict SubRelStr of L; ::_thesis: ( R is Element of S iff ( R is infs-inheriting & R is full ) ) R is Element of (Sub L) by Def2; hence ( R is Element of S iff ( R is infs-inheriting & R is full ) ) by A3; ::_thesis: verum end; correctness uniqueness for b1, b2 being non empty strict full SubRelStr of Sub L st ( for R being strict SubRelStr of L holds ( R is Element of b1 iff ( R is infs-inheriting & R is full ) ) ) & ( for R being strict SubRelStr of L holds ( R is Element of b2 iff ( R is infs-inheriting & R is full ) ) ) holds b1 = b2; proof defpred S1[ set ] means \$1 is strict full infs-inheriting SubRelStr of L; let S1, S2 be non empty strict full SubRelStr of Sub L; ::_thesis: ( ( for R being strict SubRelStr of L holds ( R is Element of S1 iff ( R is infs-inheriting & R is full ) ) ) & ( for R being strict SubRelStr of L holds ( R is Element of S2 iff ( R is infs-inheriting & R is full ) ) ) implies S1 = S2 ) assume that A4: for R being strict SubRelStr of L holds ( R is Element of S1 iff ( R is infs-inheriting & R is full ) ) and A5: for R being strict SubRelStr of L holds ( R is Element of S2 iff ( R is infs-inheriting & R is full ) ) ; ::_thesis: S1 = S2 A6: now__::_thesis:_for_x_being_set_holds_ (_x_is_Element_of_S2_iff_S1[x]_) let x be set ; ::_thesis: ( x is Element of S2 iff S1[x] ) ( x is Element of S2 implies x is Element of (Sub L) ) by YELLOW_0:58; then ( x is Element of S2 implies x is strict SubRelStr of L ) by Def2; hence ( x is Element of S2 iff S1[x] ) by A5; ::_thesis: verum end; A7: now__::_thesis:_for_x_being_set_holds_ (_x_is_Element_of_S1_iff_S1[x]_) let x be set ; ::_thesis: ( x is Element of S1 iff S1[x] ) ( x is Element of S1 implies x is Element of (Sub L) ) by YELLOW_0:58; then ( x is Element of S1 implies x is strict SubRelStr of L ) by Def2; hence ( x is Element of S1 iff S1[x] ) by A4; ::_thesis: verum end; RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) from WAYBEL10:sch_3(A7, A6); hence S1 = S2 ; ::_thesis: verum end; end; :: deftheorem Def3 defines ClosureSystems WAYBEL10:def_3_:_ for L being non empty RelStr for b2 being non empty strict full SubRelStr of Sub L holds ( b2 = ClosureSystems L iff for R being strict SubRelStr of L holds ( R is Element of b2 iff ( R is infs-inheriting & R is full ) ) ); theorem Th16: :: WAYBEL10:16 for L being non empty RelStr for x being set holds ( x is Element of (ClosureSystems L) iff x is strict closure System of L ) proof let L be non empty RelStr ; ::_thesis: for x being set holds ( x is Element of (ClosureSystems L) iff x is strict closure System of L ) let x be set ; ::_thesis: ( x is Element of (ClosureSystems L) iff x is strict closure System of L ) ( x is Element of (ClosureSystems L) implies x is Element of (Sub L) ) by YELLOW_0:58; then ( x is Element of (ClosureSystems L) implies x is strict SubRelStr of L ) by Def2; hence ( x is Element of (ClosureSystems L) iff x is strict closure System of L ) by Def3; ::_thesis: verum end; theorem Th17: :: WAYBEL10:17 for L being non empty RelStr for R being RelStr for x, y being Element of (ClosureSystems L) st y = R holds ( x <= y iff x is SubRelStr of R ) proof let L be non empty RelStr ; ::_thesis: for R being RelStr for x, y being Element of (ClosureSystems L) st y = R holds ( x <= y iff x is SubRelStr of R ) let R be RelStr ; ::_thesis: for x, y being Element of (ClosureSystems L) st y = R holds ( x <= y iff x is SubRelStr of R ) let x, y be Element of (ClosureSystems L); ::_thesis: ( y = R implies ( x <= y iff x is SubRelStr of R ) ) reconsider a = x, b = y as Element of (Sub L) by YELLOW_0:58; ( x <= y iff a <= b ) by YELLOW_0:59, YELLOW_0:60; hence ( y = R implies ( x <= y iff x is SubRelStr of R ) ) by Th15; ::_thesis: verum end; begin registration let L be non empty Poset; let h be closure Function of L,L; cluster Image h -> infs-inheriting ; coherence Image h is closure by WAYBEL_1:53; end; definition let L be non empty Poset; func ClImageMap L -> Function of (ClOpers L),((ClosureSystems L) opp) means :Def4: :: WAYBEL10:def 4 for c being closure Function of L,L holds it . c = Image c; existence ex b1 being Function of (ClOpers L),((ClosureSystems L) opp) st for c being closure Function of L,L holds b1 . c = Image c proof defpred S1[ set , set ] means ex c being closure Function of L,L st ( c = \$1 & \$2 = Image c ); A1: now__::_thesis:_for_x_being_Element_of_(ClOpers_L)_ex_b_being_Element_of_the_carrier_of_((ClosureSystems_L)_~)_st_S1[x,b] let x be Element of (ClOpers L); ::_thesis: ex b being Element of the carrier of ((ClosureSystems L) ~) st S1[x,b] reconsider c = x as closure Function of L,L by Th10; reconsider a = Image c as Element of (ClosureSystems L) by Th16; take b = a ~ ; ::_thesis: S1[x,b] thus S1[x,b] ; ::_thesis: verum end; consider f being Function of (ClOpers L),((ClosureSystems L) opp) such that A2: for x being Element of (ClOpers L) holds S1[x,f . x] from FUNCT_2:sch_3(A1); take f ; ::_thesis: for c being closure Function of L,L holds f . c = Image c let c be closure Function of L,L; ::_thesis: f . c = Image c c is Element of (ClOpers L) by Th10; then ex c1 being closure Function of L,L st ( c1 = c & f . c = Image c1 ) by A2; hence f . c = Image c ; ::_thesis: verum end; correctness uniqueness for b1, b2 being Function of (ClOpers L),((ClosureSystems L) opp) st ( for c being closure Function of L,L holds b1 . c = Image c ) & ( for c being closure Function of L,L holds b2 . c = Image c ) holds b1 = b2; proof let f1, f2 be Function of (ClOpers L),((ClosureSystems L) opp); ::_thesis: ( ( for c being closure Function of L,L holds f1 . c = Image c ) & ( for c being closure Function of L,L holds f2 . c = Image c ) implies f1 = f2 ) assume that A3: for c being closure Function of L,L holds f1 . c = Image c and A4: for c being closure Function of L,L holds f2 . c = Image c ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_Element_of_(ClOpers_L)_holds_f1_._x_=_f2_._x let x be Element of (ClOpers L); ::_thesis: f1 . x = f2 . x reconsider c = x as closure Function of L,L by Th10; thus f1 . x = Image c by A3 .= f2 . x by A4 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines ClImageMap WAYBEL10:def_4_:_ for L being non empty Poset for b2 being Function of (ClOpers L),((ClosureSystems L) opp) holds ( b2 = ClImageMap L iff for c being closure Function of L,L holds b2 . c = Image c ); definition let L be non empty RelStr ; let S be SubRelStr of L; func closure_op S -> Function of L,L means :Def5: :: WAYBEL10:def 5 for x being Element of L holds it . x = "/\" (((uparrow x) /\ the carrier of S),L); existence ex b1 being Function of L,L st for x being Element of L holds b1 . x = "/\" (((uparrow x) /\ the carrier of S),L) proof deffunc H1( Element of L) -> Element of the carrier of L = "/\" (((uparrow \$1) /\ the carrier of S),L); thus ex f being Function of L,L st for x being Element of L holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of L,L st ( for x being Element of L holds b1 . x = "/\" (((uparrow x) /\ the carrier of S),L) ) & ( for x being Element of L holds b2 . x = "/\" (((uparrow x) /\ the carrier of S),L) ) holds b1 = b2 proof let f1, f2 be Function of L,L; ::_thesis: ( ( for x being Element of L holds f1 . x = "/\" (((uparrow x) /\ the carrier of S),L) ) & ( for x being Element of L holds f2 . x = "/\" (((uparrow x) /\ the carrier of S),L) ) implies f1 = f2 ) assume that A1: for x being Element of L holds f1 . x = "/\" (((uparrow x) /\ the carrier of S),L) and A2: for x being Element of L holds f2 . x = "/\" (((uparrow x) /\ the carrier of S),L) ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_Element_of_L_holds_f1_._x_=_f2_._x let x be Element of L; ::_thesis: f1 . x = f2 . x thus f1 . x = "/\" (((uparrow x) /\ the carrier of S),L) by A1 .= f2 . x by A2 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def5 defines closure_op WAYBEL10:def_5_:_ for L being non empty RelStr for S being SubRelStr of L for b3 being Function of L,L holds ( b3 = closure_op S iff for x being Element of L holds b3 . x = "/\" (((uparrow x) /\ the carrier of S),L) ); registration let L be complete LATTICE; let S be closure System of L; cluster closure_op S -> closure ; coherence closure_op S is closure proof set c = closure_op S; reconsider cc = (closure_op S) * (closure_op S) as Function of L,L ; A1: now__::_thesis:_for_x_being_Element_of_L_holds_ (_(id_L)_._x_=_x_&_(id_L)_._x_<=_(closure_op_S)_._x_) let x be Element of L; ::_thesis: ( (id L) . x = x & (id L) . x <= (closure_op S) . x ) thus A2: (id L) . x = x by FUNCT_1:18; ::_thesis: (id L) . x <= (closure_op S) . x (uparrow x) /\ the carrier of S c= uparrow x by XBOOLE_1:17; then A3: x is_<=_than (uparrow x) /\ the carrier of S by YELLOW_2:2; (closure_op S) . x = "/\" (((uparrow x) /\ the carrier of S),L) by Def5; hence (id L) . x <= (closure_op S) . x by A2, A3, YELLOW_0:33; ::_thesis: verum end; now__::_thesis:_for_x_being_Element_of_L_holds_cc_._x_=_(closure_op_S)_._x let x be Element of L; ::_thesis: cc . x = (closure_op S) . x set y = (closure_op S) . x; set X = (uparrow x) /\ the carrier of S; reconsider X = (uparrow x) /\ the carrier of S as Subset of S by XBOOLE_1:17; A4: (closure_op S) . ((closure_op S) . x) = "/\" (((uparrow ((closure_op S) . x)) /\ the carrier of S),L) by Def5; (closure_op S) . x <= (closure_op S) . x ; then A5: (closure_op S) . x in uparrow ((closure_op S) . x) by WAYBEL_0:18; ex_inf_of X,L by YELLOW_0:17; then A6: "/\" (X,L) in the carrier of S by YELLOW_0:def_18; (closure_op S) . x = "/\" (((uparrow x) /\ the carrier of S),L) by Def5; then (closure_op S) . x in (uparrow ((closure_op S) . x)) /\ the carrier of S by A6, A5, XBOOLE_0:def_4; then A7: (closure_op S) . ((closure_op S) . x) <= (closure_op S) . x by A4, YELLOW_2:22; A8: (closure_op S) . ((closure_op S) . x) >= (id L) . ((closure_op S) . x) by A1; A9: (id L) . ((closure_op S) . x) = (closure_op S) . x by A1; thus cc . x = (closure_op S) . ((closure_op S) . x) by FUNCT_2:15 .= (closure_op S) . x by A7, A8, A9, ORDERS_2:2 ; ::_thesis: verum end; hence (closure_op S) * (closure_op S) = closure_op S by FUNCT_2:63; :: according to QUANTAL1:def_9,WAYBEL_1:def_13,WAYBEL_1:def_14 ::_thesis: ( closure_op S is monotone & id L <= closure_op S ) hereby :: according to WAYBEL_1:def_2 ::_thesis: id L <= closure_op S let x, y be Element of L; ::_thesis: ( x <= y implies (closure_op S) . x <= (closure_op S) . y ) A10: ex_inf_of (uparrow x) /\ the carrier of S,L by YELLOW_0:17; A11: ex_inf_of (uparrow y) /\ the carrier of S,L by YELLOW_0:17; assume x <= y ; ::_thesis: (closure_op S) . x <= (closure_op S) . y then A12: (uparrow y) /\ the carrier of S c= (uparrow x) /\ the carrier of S by WAYBEL_0:22, XBOOLE_1:26; A13: (closure_op S) . y = "/\" (((uparrow y) /\ the carrier of S),L) by Def5; (closure_op S) . x = "/\" (((uparrow x) /\ the carrier of S),L) by Def5; hence (closure_op S) . x <= (closure_op S) . y by A12, A10, A11, A13, YELLOW_0:35; ::_thesis: verum end; let x be set ; :: according to YELLOW_2:def_1 ::_thesis: ( not x in the carrier of L or ex b1, b2 being Element of the carrier of L st ( b1 = (id L) . x & b2 = (closure_op S) . x & b1 <= b2 ) ) assume x in the carrier of L ; ::_thesis: ex b1, b2 being Element of the carrier of L st ( b1 = (id L) . x & b2 = (closure_op S) . x & b1 <= b2 ) then reconsider x = x as Element of L ; (id L) . x <= (closure_op S) . x by A1; hence ex b1, b2 being Element of the carrier of L st ( b1 = (id L) . x & b2 = (closure_op S) . x & b1 <= b2 ) ; ::_thesis: verum end; end; theorem Th18: :: WAYBEL10:18 for L being complete LATTICE for S being closure System of L holds Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #) proof let L be complete LATTICE; ::_thesis: for S being closure System of L holds Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #) let S be non empty full infs-inheriting SubRelStr of L; ::_thesis: Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #) the carrier of (Image (closure_op S)) = the carrier of S proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of S c= the carrier of (Image (closure_op S)) let x be set ; ::_thesis: ( x in the carrier of (Image (closure_op S)) implies x in the carrier of S ) assume x in the carrier of (Image (closure_op S)) ; ::_thesis: x in the carrier of S then reconsider a = x as Element of (Image (closure_op S)) ; consider b being Element of L such that A1: a = (closure_op S) . b by YELLOW_2:10; set X = (uparrow b) /\ the carrier of S; reconsider X = (uparrow b) /\ the carrier of S as Subset of S by XBOOLE_1:17; A2: ex_inf_of X,L by YELLOW_0:17; a = "/\" (X,L) by A1, Def5; hence x in the carrier of S by A2, YELLOW_0:def_18; ::_thesis: verum end; set c = closure_op S; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of S or x in the carrier of (Image (closure_op S)) ) assume x in the carrier of S ; ::_thesis: x in the carrier of (Image (closure_op S)) then reconsider a = x as Element of S ; reconsider a = a as Element of L by YELLOW_0:58; set X = (uparrow a) /\ the carrier of S; A3: (id L) . a = a by FUNCT_1:18; a <= a ; then a in uparrow a by WAYBEL_0:18; then A4: a in (uparrow a) /\ the carrier of S by XBOOLE_0:def_4; (closure_op S) . a = "/\" (((uparrow a) /\ the carrier of S),L) by Def5; then A5: (closure_op S) . a <= a by A4, YELLOW_2:22; id L <= closure_op S by WAYBEL_1:def_14; then a <= (closure_op S) . a by A3, YELLOW_2:9; then A6: a = (closure_op S) . a by A5, ORDERS_2:2; dom (closure_op S) = the carrier of L by FUNCT_2:def_1; then a in rng (closure_op S) by A6, FUNCT_1:def_3; hence x in the carrier of (Image (closure_op S)) by YELLOW_0:def_15; ::_thesis: verum end; hence Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_0:57; ::_thesis: verum end; theorem Th19: :: WAYBEL10:19 for L being complete LATTICE for c being closure Function of L,L holds closure_op (Image c) = c proof let L be complete LATTICE; ::_thesis: for c being closure Function of L,L holds closure_op (Image c) = c let c be closure Function of L,L; ::_thesis: closure_op (Image c) = c now__::_thesis:_for_x_being_Element_of_L_holds_(closure_op_(Image_c))_._x_=_c_._x let x be Element of L; ::_thesis: (closure_op (Image c)) . x = c . x A1: id L <= c by WAYBEL_1:def_14; x = (id L) . x by FUNCT_1:18; then x <= c . x by A1, YELLOW_2:9; then A2: c . x in uparrow x by WAYBEL_0:18; dom c = the carrier of L by FUNCT_2:def_1; then c . x in rng c by FUNCT_1:def_3; then c . x in (uparrow x) /\ (rng c) by A2, XBOOLE_0:def_4; then A3: c . x >= "/\" (((uparrow x) /\ (rng c)),L) by YELLOW_2:22; c . x is_<=_than (uparrow x) /\ (rng c) proof let z be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not z in (uparrow x) /\ (rng c) or c . x <= z ) assume A4: z in (uparrow x) /\ (rng c) ; ::_thesis: c . x <= z then z in rng c by XBOOLE_0:def_4; then consider a being set such that A5: a in dom c and A6: z = c . a by FUNCT_1:def_3; reconsider a = a as Element of L by A5; z in uparrow x by A4, XBOOLE_0:def_4; then x <= c . a by A6, WAYBEL_0:18; then c . x <= c . (c . a) by WAYBEL_1:def_2; hence c . x <= z by A6, YELLOW_2:18; ::_thesis: verum end; then A7: c . x <= "/\" (((uparrow x) /\ (rng c)),L) by YELLOW_0:33; rng c = the carrier of (Image c) by YELLOW_0:def_15; hence (closure_op (Image c)) . x = "/\" (((uparrow x) /\ (rng c)),L) by Def5 .= c . x by A3, A7, ORDERS_2:2 ; ::_thesis: verum end; hence closure_op (Image c) = c by FUNCT_2:63; ::_thesis: verum end; registration let L be complete LATTICE; cluster ClImageMap L -> V7() ; coherence ClImageMap L is one-to-one proof let x, y be Element of (ClOpers L); :: according to WAYBEL_1:def_1 ::_thesis: ( not (ClImageMap L) . x = (ClImageMap L) . y or x = y ) reconsider a = x, b = y as closure Function of L,L by Th10; set f = ClImageMap L; assume (ClImageMap L) . x = (ClImageMap L) . y ; ::_thesis: x = y then Image a = (ClImageMap L) . y by Def4 .= Image b by Def4 ; hence x = closure_op (Image b) by Th19 .= y by Th19 ; ::_thesis: verum end; end; theorem Th20: :: WAYBEL10:20 for L being complete LATTICE holds (ClImageMap L) " is Function of ((ClosureSystems L) opp),(ClOpers L) proof let L be complete LATTICE; ::_thesis: (ClImageMap L) " is Function of ((ClosureSystems L) opp),(ClOpers L) set f = ClImageMap L; A1: rng ((ClImageMap L) ") = dom (ClImageMap L) by FUNCT_1:33; A2: dom (ClImageMap L) = the carrier of (ClOpers L) by FUNCT_2:def_1; the carrier of ((ClosureSystems L) opp) c= rng (ClImageMap L) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((ClosureSystems L) opp) or x in rng (ClImageMap L) ) assume x in the carrier of ((ClosureSystems L) opp) ; ::_thesis: x in rng (ClImageMap L) then reconsider x = x as Element of ((ClosureSystems L) opp) ; reconsider x = x as strict full infs-inheriting SubRelStr of L by Th16; A3: closure_op x is Element of (ClOpers L) by Th10; (ClImageMap L) . (closure_op x) = Image (closure_op x) by Def4 .= x by Th18 ; hence x in rng (ClImageMap L) by A2, A3, FUNCT_1:def_3; ::_thesis: verum end; then A4: the carrier of ((ClosureSystems L) opp) = rng (ClImageMap L) by XBOOLE_0:def_10; dom ((ClImageMap L) ") = rng (ClImageMap L) by FUNCT_1:33; hence (ClImageMap L) " is Function of ((ClosureSystems L) opp),(ClOpers L) by A1, A4, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; theorem Th21: :: WAYBEL10:21 for L being complete LATTICE for S being strict closure System of L holds ((ClImageMap L) ") . S = closure_op S proof let L be complete LATTICE; ::_thesis: for S being strict closure System of L holds ((ClImageMap L) ") . S = closure_op S let S be strict full infs-inheriting SubRelStr of L; ::_thesis: ((ClImageMap L) ") . S = closure_op S A1: closure_op S is Element of (ClOpers L) by Th10; (ClImageMap L) . (closure_op S) = Image (closure_op S) by Def4 .= S by Th18 ; hence ((ClImageMap L) ") . S = closure_op S by A1, FUNCT_2:26; ::_thesis: verum end; registration let L be complete LATTICE; cluster ClImageMap L -> isomorphic ; correctness coherence ClImageMap L is isomorphic ; proof set f = ClImageMap L; set S = ClOpers L; set T = (ClosureSystems L) opp ; reconsider g = (ClImageMap L) " as Function of ((ClosureSystems L) opp),(ClOpers L) by Th20; percases ( ( not ClOpers L is empty & not (ClosureSystems L) opp is empty ) or ClOpers L is empty or (ClosureSystems L) opp is empty ) ; :: according to WAYBEL_0:def_38 case ( not ClOpers L is empty & not (ClosureSystems L) opp is empty ) ; ::_thesis: ( ClImageMap L is one-to-one & ClImageMap L is monotone & ex b1 being Element of bool [: the carrier of ((ClosureSystems L) opp), the carrier of (ClOpers L):] st ( b1 = (ClImageMap L) " & b1 is monotone ) ) thus ClImageMap L is V7() ; ::_thesis: ( ClImageMap L is monotone & ex b1 being Element of bool [: the carrier of ((ClosureSystems L) opp), the carrier of (ClOpers L):] st ( b1 = (ClImageMap L) " & b1 is monotone ) ) thus ClImageMap L is monotone ::_thesis: ex b1 being Element of bool [: the carrier of ((ClosureSystems L) opp), the carrier of (ClOpers L):] st ( b1 = (ClImageMap L) " & b1 is monotone ) proof let x, y be Element of (ClOpers L); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (ClImageMap L) . x <= (ClImageMap L) . y ) reconsider c = x, d = y as closure Function of L,L by Th10; A1: (ClImageMap L) . y = Image d by Def4; assume x <= y ; ::_thesis: (ClImageMap L) . x <= (ClImageMap L) . y then c <= d by Th12; then A2: Image d is SubRelStr of Image c by Th14; (ClImageMap L) . x = Image c by Def4; then ~ ((ClImageMap L) . x) >= ~ ((ClImageMap L) . y) by A2, A1, Th17; hence (ClImageMap L) . x <= (ClImageMap L) . y by YELLOW_7:1; ::_thesis: verum end; take g ; ::_thesis: ( g = (ClImageMap L) " & g is monotone ) thus g = (ClImageMap L) " ; ::_thesis: g is monotone thus g is monotone ::_thesis: verum proof let x, y be Element of ((ClosureSystems L) opp); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or g . x <= g . y ) reconsider A = ~ x, B = ~ y as strict full infs-inheriting SubRelStr of L by Th16; A3: B = Image (closure_op B) by Th18; A4: g . A = closure_op A by Th21; assume x <= y ; ::_thesis: g . x <= g . y then ~ y <= ~ x by YELLOW_7:1; then A5: B is SubRelStr of A by Th17; A6: g . B = closure_op B by Th21; A = Image (closure_op A) by Th18; then closure_op A <= closure_op B by A5, A3, Th14; hence g . x <= g . y by A4, A6, Th12; ::_thesis: verum end; end; case ( ClOpers L is empty or (ClosureSystems L) opp is empty ) ; ::_thesis: ( ClOpers L is empty & (ClosureSystems L) opp is empty ) hence ( ClOpers L is empty & (ClosureSystems L) opp is empty ) ; ::_thesis: verum end; end; end; end; theorem :: WAYBEL10:22 for L being complete LATTICE holds ClOpers L,(ClosureSystems L) opp are_isomorphic proof let L be complete LATTICE; ::_thesis: ClOpers L,(ClosureSystems L) opp are_isomorphic take ClImageMap L ; :: according to WAYBEL_1:def_8 ::_thesis: ClImageMap L is isomorphic thus ClImageMap L is isomorphic ; ::_thesis: verum end; begin theorem Th23: :: WAYBEL10:23 for L being RelStr for S being full SubRelStr of L for X being Subset of S holds ( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) ) proof let L be RelStr ; ::_thesis: for S being full SubRelStr of L for X being Subset of S holds ( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) ) let S be full SubRelStr of L; ::_thesis: for X being Subset of S holds ( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) ) let X be Subset of S; ::_thesis: ( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) ) hereby ::_thesis: ( X is filtered Subset of L implies X is filtered ) assume A1: X is directed Subset of L ; ::_thesis: X is directed thus X is directed ::_thesis: verum proof A2: the carrier of S c= the carrier of L by YELLOW_0:def_13; let x, y be Element of S; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in X or not y in X or ex b1 being Element of the carrier of S st ( b1 in X & x <= b1 & y <= b1 ) ) assume that A3: x in X and A4: y in X ; ::_thesis: ex b1 being Element of the carrier of S st ( b1 in X & x <= b1 & y <= b1 ) A5: y in the carrier of S by A3; x in the carrier of S by A3; then reconsider x9 = x, y9 = y as Element of L by A5, A2; consider z being Element of L such that A6: z in X and A7: z >= x9 and A8: z >= y9 by A1, A3, A4, WAYBEL_0:def_1; reconsider z = z as Element of S by A6; take z ; ::_thesis: ( z in X & x <= z & y <= z ) thus ( z in X & x <= z & y <= z ) by A6, A7, A8, YELLOW_0:60; ::_thesis: verum end; end; assume A9: X is filtered Subset of L ; ::_thesis: X is filtered A10: the carrier of S c= the carrier of L by YELLOW_0:def_13; let x, y be Element of S; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in X or not y in X or ex b1 being Element of the carrier of S st ( b1 in X & b1 <= x & b1 <= y ) ) assume that A11: x in X and A12: y in X ; ::_thesis: ex b1 being Element of the carrier of S st ( b1 in X & b1 <= x & b1 <= y ) A13: y in the carrier of S by A11; x in the carrier of S by A11; then reconsider x9 = x, y9 = y as Element of L by A13, A10; consider z being Element of L such that A14: z in X and A15: z <= x9 and A16: z <= y9 by A9, A11, A12, WAYBEL_0:def_2; reconsider z = z as Element of S by A14; take z ; ::_thesis: ( z in X & z <= x & z <= y ) thus ( z in X & z <= x & z <= y ) by A14, A15, A16, YELLOW_0:60; ::_thesis: verum end; theorem Th24: :: WAYBEL10:24 for L being complete LATTICE for S being closure System of L holds ( closure_op S is directed-sups-preserving iff S is directed-sups-inheriting ) proof 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 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; (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, WAYBEL_0:def_4; ::_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 set 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 end; theorem :: WAYBEL10:25 for L being complete LATTICE for h being closure Function of L,L holds ( h is directed-sups-preserving iff Image h is directed-sups-inheriting ) proof let L be complete LATTICE; ::_thesis: for h being closure Function of L,L holds ( h is directed-sups-preserving iff Image h is directed-sups-inheriting ) let h be closure Function of L,L; ::_thesis: ( h is directed-sups-preserving iff Image h is directed-sups-inheriting ) closure_op (Image h) = h by Th19; hence ( h is directed-sups-preserving iff Image h is directed-sups-inheriting ) by Th24; ::_thesis: verum end; registration let L be complete LATTICE; let S be closure directed-sups-inheriting System of L; cluster closure_op S -> directed-sups-preserving ; coherence closure_op S is directed-sups-preserving by Th24; end; registration let L be complete LATTICE; let h be directed-sups-preserving closure Function of L,L; cluster Image h -> directed-sups-inheriting ; coherence Image h is directed-sups-inheriting proof h = closure_op (Image h) by Th19; hence Image h is directed-sups-inheriting by Th24; ::_thesis: verum end; end; definition let L be non empty reflexive RelStr ; func DsupClOpers L -> non empty strict full SubRelStr of ClOpers L means :Def6: :: WAYBEL10:def 6 for f being closure Function of L,L holds ( f is Element of it iff f is directed-sups-preserving ); existence ex b1 being non empty strict full SubRelStr of ClOpers L st for f being closure Function of L,L holds ( f is Element of b1 iff f is directed-sups-preserving ) proof defpred S1[ set ] means \$1 is directed-sups-preserving Function of L,L; set h = the directed-sups-preserving closure Function of L,L; the directed-sups-preserving closure Function of L,L is Element of (ClOpers L) by Def1; then A1: the directed-sups-preserving closure Function of L,L in the carrier of (ClOpers L) ; A2: S1[ the directed-sups-preserving closure Function of L,L] ; consider S being non empty strict full SubRelStr of ClOpers L such that A3: for f being Element of (ClOpers L) holds ( f is Element of S iff S1[f] ) from WAYBEL10:sch_1(A2, A1); take S ; ::_thesis: for f being closure Function of L,L holds ( f is Element of S iff f is directed-sups-preserving ) let f be closure Function of L,L; ::_thesis: ( f is Element of S iff f is directed-sups-preserving ) hereby ::_thesis: ( f is directed-sups-preserving implies f is Element of S ) assume A4: f is Element of S ; ::_thesis: f is directed-sups-preserving then f is Element of (ClOpers L) by YELLOW_0:58; hence f is directed-sups-preserving by A3, A4; ::_thesis: verum end; assume A5: f is directed-sups-preserving ; ::_thesis: f is Element of S f is Element of (ClOpers L) by Def1; hence f is Element of S by A3, A5; ::_thesis: verum end; correctness uniqueness for b1, b2 being non empty strict full SubRelStr of ClOpers L st ( for f being closure Function of L,L holds ( f is Element of b1 iff f is directed-sups-preserving ) ) & ( for f being closure Function of L,L holds ( f is Element of b2 iff f is directed-sups-preserving ) ) holds b1 = b2; proof defpred S1[ set ] means \$1 is directed-sups-preserving closure Function of L,L; let S1, S2 be non empty strict full SubRelStr of ClOpers L; ::_thesis: ( ( for f being closure Function of L,L holds ( f is Element of S1 iff f is directed-sups-preserving ) ) & ( for f being closure Function of L,L holds ( f is Element of S2 iff f is directed-sups-preserving ) ) implies S1 = S2 ) assume that A6: for f being closure Function of L,L holds ( f is Element of S1 iff f is directed-sups-preserving ) and A7: for f being closure Function of L,L holds ( f is Element of S2 iff f is directed-sups-preserving ) ; ::_thesis: S1 = S2 A8: now__::_thesis:_for_f_being_set_holds_ (_f_is_Element_of_S2_iff_S1[f]_) let f be set ; ::_thesis: ( f is Element of S2 iff S1[f] ) ( f is Element of S2 implies f is Element of (ClOpers L) ) by YELLOW_0:58; then ( f is Element of S2 implies f is closure Function of L,L ) by Th10; hence ( f is Element of S2 iff S1[f] ) by A7; ::_thesis: verum end; A9: now__::_thesis:_for_f_being_set_holds_ (_f_is_Element_of_S1_iff_S1[f]_) let f be set ; ::_thesis: ( f is Element of S1 iff S1[f] ) ( f is Element of S1 implies f is Element of (ClOpers L) ) by YELLOW_0:58; then ( f is Element of S1 implies f is closure Function of L,L ) by Th10; hence ( f is Element of S1 iff S1[f] ) by A6; ::_thesis: verum end; RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) from WAYBEL10:sch_3(A9, A8); hence S1 = S2 ; ::_thesis: verum end; end; :: deftheorem Def6 defines DsupClOpers WAYBEL10:def_6_:_ for L being non empty reflexive RelStr for b2 being non empty strict full SubRelStr of ClOpers L holds ( b2 = DsupClOpers L iff for f being closure Function of L,L holds ( f is Element of b2 iff f is directed-sups-preserving ) ); theorem Th26: :: WAYBEL10:26 for L being non empty reflexive RelStr for x being set holds ( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L ) proof let L be non empty reflexive RelStr ; ::_thesis: for x being set holds ( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L ) let x be set ; ::_thesis: ( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L ) ( x is Element of (ClOpers L) iff x is closure Function of L,L ) by Th10; hence ( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L ) by Def6, YELLOW_0:58; ::_thesis: verum end; definition let L be non empty RelStr ; func Subalgebras L -> non empty strict full SubRelStr of ClosureSystems L means :Def7: :: WAYBEL10:def 7 for R being strict closure System of L holds ( R is Element of it iff R is directed-sups-inheriting ); existence ex b1 being non empty strict full SubRelStr of ClosureSystems L st for R being strict closure System of L holds ( R is Element of b1 iff R is directed-sups-inheriting ) proof defpred S1[ set ] means \$1 is directed-sups-inheriting SubRelStr of L; set SL = subrelstr ([#] L); subrelstr ([#] L) is Element of (ClosureSystems L) by Def3; then A1: subrelstr ([#] L) in the carrier of (ClosureSystems L) ; A2: S1[ subrelstr ([#] L)] ; consider S being non empty strict full SubRelStr of ClosureSystems L such that A3: for x being Element of (ClosureSystems L) holds ( x is Element of S iff S1[x] ) from WAYBEL10:sch_1(A2, A1); take S ; ::_thesis: for R being strict closure System of L holds ( R is Element of S iff R is directed-sups-inheriting ) let R be strict closure System of L; ::_thesis: ( R is Element of S iff R is directed-sups-inheriting ) R is Element of (ClosureSystems L) by Def3; hence ( R is Element of S iff R is directed-sups-inheriting ) by A3; ::_thesis: verum end; correctness uniqueness for b1, b2 being non empty strict full SubRelStr of ClosureSystems L st ( for R being strict closure System of L holds ( R is Element of b1 iff R is directed-sups-inheriting ) ) & ( for R being strict closure System of L holds ( R is Element of b2 iff R is directed-sups-inheriting ) ) holds b1 = b2; proof defpred S1[ set ] means \$1 is strict closure directed-sups-inheriting System of L; let S1, S2 be non empty strict full SubRelStr of ClosureSystems L; ::_thesis: ( ( for R being strict closure System of L holds ( R is Element of S1 iff R is directed-sups-inheriting ) ) & ( for R being strict closure System of L holds ( R is Element of S2 iff R is directed-sups-inheriting ) ) implies S1 = S2 ) assume that A4: for R being strict closure System of L holds ( R is Element of S1 iff R is directed-sups-inheriting ) and A5: for R being strict closure System of L holds ( R is Element of S2 iff R is directed-sups-inheriting ) ; ::_thesis: S1 = S2 A6: now__::_thesis:_for_x_being_set_holds_ (_x_is_Element_of_S2_iff_S1[x]_) let x be set ; ::_thesis: ( x is Element of S2 iff S1[x] ) ( x is Element of S2 implies x is Element of (ClosureSystems L) ) by YELLOW_0:58; then ( x is Element of S2 implies x is strict closure System of L ) by Th16; hence ( x is Element of S2 iff S1[x] ) by A5; ::_thesis: verum end; A7: now__::_thesis:_for_x_being_set_holds_ (_x_is_Element_of_S1_iff_S1[x]_) let x be set ; ::_thesis: ( x is Element of S1 iff S1[x] ) ( x is Element of S1 implies x is Element of (ClosureSystems L) ) by YELLOW_0:58; then ( x is Element of S1 implies x is strict closure System of L ) by Th16; hence ( x is Element of S1 iff S1[x] ) by A4; ::_thesis: verum end; RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) from WAYBEL10:sch_3(A7, A6); hence S1 = S2 ; ::_thesis: verum end; end; :: deftheorem Def7 defines Subalgebras WAYBEL10:def_7_:_ for L being non empty RelStr for b2 being non empty strict full SubRelStr of ClosureSystems L holds ( b2 = Subalgebras L iff for R being strict closure System of L holds ( R is Element of b2 iff R is directed-sups-inheriting ) ); theorem Th27: :: WAYBEL10:27 for L being non empty RelStr for x being set holds ( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L ) proof let L be non empty RelStr ; ::_thesis: for x being set holds ( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L ) let x be set ; ::_thesis: ( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L ) ( x is Element of (ClosureSystems L) iff x is strict closure System of L ) by Th16; hence ( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L ) by Def7, YELLOW_0:58; ::_thesis: verum end; theorem Th28: :: WAYBEL10:28 for L being complete LATTICE holds Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp proof let L be complete LATTICE; ::_thesis: Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp defpred S1[ set ] means \$1 is strict closure directed-sups-inheriting System of L; A1: now__::_thesis:_for_a_being_set_holds_ (_(_a_is_Element_of_(Image_((ClImageMap_L)_|_(DsupClOpers_L)))_implies_S1[a]_)_&_(_S1[a]_implies_a_is_Element_of_(Image_((ClImageMap_L)_|_(DsupClOpers_L)))_)_) let a be set ; ::_thesis: ( ( a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) implies S1[a] ) & ( S1[a] implies a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) ) ) hereby ::_thesis: ( S1[a] implies a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) ) assume a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) ; ::_thesis: S1[a] then consider x being Element of (DsupClOpers L) such that A2: ((ClImageMap L) | (DsupClOpers L)) . x = a by YELLOW_2:10; reconsider x = x as directed-sups-preserving closure Function of L,L by Th26; a = (ClImageMap L) . x by A2, Th6 .= Image x by Def4 ; hence S1[a] ; ::_thesis: verum end; assume S1[a] ; ::_thesis: a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) then reconsider S = a as strict closure directed-sups-inheriting System of L ; reconsider x = closure_op S as Element of (DsupClOpers L) by Th26; S = Image (closure_op S) by Th18 .= (ClImageMap L) . (closure_op S) by Def4 .= ((ClImageMap L) | (DsupClOpers L)) . x by Th6 ; then S in rng ((ClImageMap L) | (DsupClOpers L)) by FUNCT_2:4; hence a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) by YELLOW_0:def_15; ::_thesis: verum end; A3: for a being set holds ( a is Element of ((Subalgebras L) opp) iff S1[a] ) by Th27; RelStr(# the carrier of (Image ((ClImageMap L) | (DsupClOpers L))), the InternalRel of (Image ((ClImageMap L) | (DsupClOpers L))) #) = RelStr(# the carrier of ((Subalgebras L) opp), the InternalRel of ((Subalgebras L) opp) #) from WAYBEL10:sch_3(A1, A3); hence Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp ; ::_thesis: verum end; registration let L be complete LATTICE; cluster corestr ((ClImageMap L) | (DsupClOpers L)) -> isomorphic ; coherence corestr ((ClImageMap L) | (DsupClOpers L)) is isomorphic proof set f = ClImageMap L; set R = DsupClOpers L; set g = corestr ((ClImageMap L) | (DsupClOpers L)); percases ( ( not DsupClOpers L is empty & not Image ((ClImageMap L) | (DsupClOpers L)) is empty ) or DsupClOpers L is empty or Image ((ClImageMap L) | (DsupClOpers L)) is empty ) ; :: according to WAYBEL_0:def_38 case ( not DsupClOpers L is empty & not Image ((ClImageMap L) | (DsupClOpers L)) is empty ) ; ::_thesis: ( corestr ((ClImageMap L) | (DsupClOpers L)) is one-to-one & corestr ((ClImageMap L) | (DsupClOpers L)) is monotone & ex b1 being Element of bool [: the carrier of (Image ((ClImageMap L) | (DsupClOpers L))), the carrier of (DsupClOpers L):] st ( b1 = (corestr ((ClImageMap L) | (DsupClOpers L))) " & b1 is monotone ) ) (ClImageMap L) | (DsupClOpers L) is V7() by Th7; hence ( corestr ((ClImageMap L) | (DsupClOpers L)) is V7() & corestr ((ClImageMap L) | (DsupClOpers L)) is monotone ) by WAYBEL_1:30; ::_thesis: ex b1 being Element of bool [: the carrier of (Image ((ClImageMap L) | (DsupClOpers L))), the carrier of (DsupClOpers L):] st ( b1 = (corestr ((ClImageMap L) | (DsupClOpers L))) " & b1 is monotone ) consider f9 being Function of ((ClosureSystems L) opp),(ClOpers L) such that A1: f9 = (ClImageMap L) " and f9 is monotone by WAYBEL_0:def_38; reconsider h = f9 | (Image ((ClImageMap L) | (DsupClOpers L))) as Function of (Image ((ClImageMap L) | (DsupClOpers L))),(DsupClOpers L) by A1, Th8; take h ; ::_thesis: ( h = (corestr ((ClImageMap L) | (DsupClOpers L))) " & h is monotone ) thus h = ((ClImageMap L) | (DsupClOpers L)) " by A1, Th8 .= (corestr ((ClImageMap L) | (DsupClOpers L))) " by WAYBEL_1:30 ; ::_thesis: h is monotone let x, y be Element of (Image ((ClImageMap L) | (DsupClOpers L))); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or h . x <= h . y ) reconsider a = x, b = y as Element of ((ClosureSystems L) opp) by YELLOW_0:58; reconsider A = ~ a, B = ~ b as strict closure System of L by Th16; reconsider i = closure_op A, j = closure_op B as Element of (ClOpers L) by Th10; f9 . y = j by A1, Th21; then A2: h . y = j by Th6; assume x <= y ; ::_thesis: h . x <= h . y then a <= b by YELLOW_0:59; then ~ a >= ~ b by YELLOW_7:1; then A3: B is SubRelStr of A by Th17; A4: B = Image (closure_op B) by Th18; A = Image (closure_op A) by Th18; then closure_op A <= closure_op B by A3, A4, Th14; then A5: i <= j by Th12; f9 . x = i by A1, Th21; then h . x = i by Th6; hence h . x <= h . y by A2, A5, YELLOW_0:60; ::_thesis: verum end; case ( DsupClOpers L is empty or Image ((ClImageMap L) | (DsupClOpers L)) is empty ) ; ::_thesis: ( DsupClOpers L is empty & Image ((ClImageMap L) | (DsupClOpers L)) is empty ) hence ( DsupClOpers L is empty & Image ((ClImageMap L) | (DsupClOpers L)) is empty ) ; ::_thesis: verum end; end; end; end; theorem :: WAYBEL10:29 for L being complete LATTICE holds DsupClOpers L,(Subalgebras L) opp are_isomorphic proof let L be complete LATTICE; ::_thesis: DsupClOpers L,(Subalgebras L) opp are_isomorphic set f = (ClImageMap L) | (DsupClOpers L); reconsider g = corestr ((ClImageMap L) | (DsupClOpers L)) as Function of (DsupClOpers L),((Subalgebras L) opp) by Th28; take g ; :: according to WAYBEL_1:def_8 ::_thesis: g is isomorphic Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp by Th28; hence g is isomorphic ; ::_thesis: verum end;