:: WAYBEL_2 semantic presentation begin registration let X, Y be non empty set ; let f be Function of X,Y; let Z be non empty Subset of X; clusterf .: Z -> non empty ; coherence not f .: Z is empty proof set x = the Element of Z; A1: dom f = X by FUNCT_2:def_1; thus not f .: Z is empty by A1; ::_thesis: verum end; end; registration cluster non empty reflexive connected -> non empty with_suprema with_infima for RelStr ; coherence for b1 being non empty RelStr st b1 is reflexive & b1 is connected holds ( b1 is with_infima & b1 is with_suprema ) proof let L be non empty RelStr ; ::_thesis: ( L is reflexive & L is connected implies ( L is with_infima & L is with_suprema ) ) assume A1: ( L is reflexive & L is connected ) ; ::_thesis: ( L is with_infima & L is with_suprema ) thus L is with_infima ::_thesis: L is with_suprema proof let x, y be Element of L; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of L st ( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of L holds ( not b2 <= x or not b2 <= y or b2 <= b1 ) ) ) percases ( x <= y or y <= x ) by A1, WAYBEL_0:def_29; supposeA2: x <= y ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of L holds ( not b2 <= x or not b2 <= y or b2 <= b1 ) ) ) take z = x; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of L holds ( not b1 <= x or not b1 <= y or b1 <= z ) ) ) thus ( z <= x & z <= y ) by A1, A2, YELLOW_0:def_1; ::_thesis: for b1 being Element of the carrier of L holds ( not b1 <= x or not b1 <= y or b1 <= z ) thus for b1 being Element of the carrier of L holds ( not b1 <= x or not b1 <= y or b1 <= z ) ; ::_thesis: verum end; supposeA3: y <= x ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of L holds ( not b2 <= x or not b2 <= y or b2 <= b1 ) ) ) take z = y; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of L holds ( not b1 <= x or not b1 <= y or b1 <= z ) ) ) thus ( z <= x & z <= y ) by A1, A3, YELLOW_0:def_1; ::_thesis: for b1 being Element of the carrier of L holds ( not b1 <= x or not b1 <= y or b1 <= z ) thus for b1 being Element of the carrier of L holds ( not b1 <= x or not b1 <= y or b1 <= z ) ; ::_thesis: verum end; end; end; let x, y be Element of L; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of L st ( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of L holds ( not x <= b2 or not y <= b2 or b1 <= b2 ) ) ) percases ( x <= y or y <= x ) by A1, WAYBEL_0:def_29; supposeA4: x <= y ; ::_thesis: ex b1 being Element of the carrier of L st ( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of L holds ( not x <= b2 or not y <= b2 or b1 <= b2 ) ) ) take z = y; ::_thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of L holds ( not x <= b1 or not y <= b1 or z <= b1 ) ) ) thus ( z >= x & z >= y ) by A1, A4, YELLOW_0:def_1; ::_thesis: for b1 being Element of the carrier of L holds ( not x <= b1 or not y <= b1 or z <= b1 ) thus for b1 being Element of the carrier of L holds ( not x <= b1 or not y <= b1 or z <= b1 ) ; ::_thesis: verum end; supposeA5: y <= x ; ::_thesis: ex b1 being Element of the carrier of L st ( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of L holds ( not x <= b2 or not y <= b2 or b1 <= b2 ) ) ) take z = x; ::_thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of L holds ( not x <= b1 or not y <= b1 or z <= b1 ) ) ) thus ( z >= x & z >= y ) by A1, A5, YELLOW_0:def_1; ::_thesis: for b1 being Element of the carrier of L holds ( not x <= b1 or not y <= b1 or z <= b1 ) thus for b1 being Element of the carrier of L holds ( not x <= b1 or not y <= b1 or z <= b1 ) ; ::_thesis: verum end; end; end; end; registration let C be Chain; cluster [#] C -> directed ; coherence [#] C is directed ; end; theorem Th1: :: WAYBEL_2:1 for L being up-complete Semilattice for D being non empty directed Subset of L for x being Element of L holds ex_sup_of {x} "/\" D,L proof let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of L for x being Element of L holds ex_sup_of {x} "/\" D,L let D be non empty directed Subset of L; ::_thesis: for x being Element of L holds ex_sup_of {x} "/\" D,L let x be Element of L; ::_thesis: ex_sup_of {x} "/\" D,L reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5; ex_sup_of xx "/\" D,L by WAYBEL_0:75; hence ex_sup_of {x} "/\" D,L ; ::_thesis: verum end; theorem :: WAYBEL_2:2 for L being up-complete sup-Semilattice for D being non empty directed Subset of L for x being Element of L holds ex_sup_of {x} "\/" D,L proof let L be up-complete sup-Semilattice; ::_thesis: for D being non empty directed Subset of L for x being Element of L holds ex_sup_of {x} "\/" D,L let D be non empty directed Subset of L; ::_thesis: for x being Element of L holds ex_sup_of {x} "\/" D,L let x be Element of L; ::_thesis: ex_sup_of {x} "\/" D,L reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5; ex_sup_of xx "\/" D,L by WAYBEL_0:75; hence ex_sup_of {x} "\/" D,L ; ::_thesis: verum end; theorem Th3: :: WAYBEL_2:3 for L being up-complete sup-Semilattice for A, B being non empty directed Subset of L holds A is_<=_than sup (A "\/" B) proof let L be up-complete sup-Semilattice; ::_thesis: for A, B being non empty directed Subset of L holds A is_<=_than sup (A "\/" B) let A, B be non empty directed Subset of L; ::_thesis: A is_<=_than sup (A "\/" B) A1: A "\/" B = { (x "\/" y) where x, y is Element of L : ( x in A & y in B ) } by YELLOW_4:def_3; set b = the Element of B; let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in A or x <= sup (A "\/" B) ) assume x in A ; ::_thesis: x <= sup (A "\/" B) then A2: x "\/" the Element of B in A "\/" B by A1; ex xx being Element of L st ( x <= xx & the Element of B <= xx & ( for c being Element of L st x <= c & the Element of B <= c holds xx <= c ) ) by LATTICE3:def_10; then A3: x <= x "\/" the Element of B by LATTICE3:def_13; ex_sup_of A "\/" B,L by WAYBEL_0:75; then A "\/" B is_<=_than sup (A "\/" B) by YELLOW_0:def_9; then x "\/" the Element of B <= sup (A "\/" B) by A2, LATTICE3:def_9; hence x <= sup (A "\/" B) by A3, YELLOW_0:def_2; ::_thesis: verum end; theorem Th4: :: WAYBEL_2:4 for L being up-complete sup-Semilattice for A, B being non empty directed Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B) proof let L be up-complete sup-Semilattice; ::_thesis: for A, B being non empty directed Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B) let A, B be non empty directed Subset of L; ::_thesis: sup (A "\/" B) = (sup A) "\/" (sup B) A1: ex_sup_of B,L by WAYBEL_0:75; then A2: B is_<=_than sup B by YELLOW_0:30; A3: ex_sup_of A,L by WAYBEL_0:75; then A is_<=_than sup A by YELLOW_0:30; then ( ex_sup_of A "\/" B,L & A "\/" B is_<=_than (sup A) "\/" (sup B) ) by A2, WAYBEL_0:75, YELLOW_4:27; then A4: sup (A "\/" B) <= (sup A) "\/" (sup B) by YELLOW_0:def_9; B is_<=_than sup (A "\/" B) by Th3; then A5: sup B <= sup (A "\/" B) by A1, YELLOW_0:30; A is_<=_than sup (A "\/" B) by Th3; then sup A <= sup (A "\/" B) by A3, YELLOW_0:30; then A6: (sup A) "\/" (sup B) <= (sup (A "\/" B)) "\/" (sup (A "\/" B)) by A5, YELLOW_3:3; sup (A "\/" B) <= sup (A "\/" B) ; then (sup (A "\/" B)) "\/" (sup (A "\/" B)) = sup (A "\/" B) by YELLOW_0:24; hence sup (A "\/" B) = (sup A) "\/" (sup B) by A4, A6, ORDERS_2:2; ::_thesis: verum end; theorem Th5: :: WAYBEL_2:5 for L being up-complete Semilattice for D being non empty directed Subset of [:L,L:] holds { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } = { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } proof let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } = { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } let D be non empty directed Subset of [:L,L:]; ::_thesis: { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } = { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } defpred S1[ set ] means ex x being Element of L st ( $1 = {x} "/\" (proj2 D) & x in proj1 D ); reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22; thus { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } c= { (sup X) where X is non empty directed Subset of L : S1[X] } :: according to XBOOLE_0:def_10 ::_thesis: { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } c= { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } or q in { (sup X) where X is non empty directed Subset of L : S1[X] } ) assume q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } ; ::_thesis: q in { (sup X) where X is non empty directed Subset of L : S1[X] } then consider x being Element of L such that A1: ( q = sup ({x} "/\" D2) & x in D1 ) ; reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5; ( not xx "/\" D2 is empty & xx "/\" D2 is directed ) ; hence q in { (sup X) where X is non empty directed Subset of L : S1[X] } by A1; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } or q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } ) assume q in { (sup X) where X is non empty directed Subset of L : S1[X] } ; ::_thesis: q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } then ex X being non empty directed Subset of L st ( q = sup X & S1[X] ) ; hence q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } ; ::_thesis: verum end; theorem Th6: :: WAYBEL_2:6 for L being Semilattice for D being non empty directed Subset of [:L,L:] holds union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D) proof let L be Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D) let D be non empty directed Subset of [:L,L:]; ::_thesis: union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D) set D1 = proj1 D; set D2 = proj2 D; defpred S1[ set ] means ex x being Element of L st ( $1 = {x} "/\" (proj2 D) & x in proj1 D ); reconsider T = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22; A1: (proj1 D) "/\" (proj2 D) = { (x "/\" y) where x, y is Element of L : ( x in proj1 D & y in proj2 D ) } by YELLOW_4:def_4; thus union { X where X is non empty directed Subset of L : S1[X] } c= (proj1 D) "/\" (proj2 D) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 D) "/\" (proj2 D) c= union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in union { X where X is non empty directed Subset of L : S1[X] } or q in (proj1 D) "/\" (proj2 D) ) assume q in union { X where X is non empty directed Subset of L : S1[X] } ; ::_thesis: q in (proj1 D) "/\" (proj2 D) then consider w being set such that A2: q in w and A3: w in { X where X is non empty directed Subset of L : S1[X] } by TARSKI:def_4; consider e being non empty directed Subset of L such that A4: w = e and A5: S1[e] by A3; consider p being Element of L such that A6: e = {p} "/\" (proj2 D) and A7: p in proj1 D by A5; {p} "/\" (proj2 D) = { (p "/\" y) where y is Element of L : y in proj2 D } by YELLOW_4:42; then ex y being Element of L st ( q = p "/\" y & y in proj2 D ) by A2, A4, A6; hence q in (proj1 D) "/\" (proj2 D) by A1, A7; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (proj1 D) "/\" (proj2 D) or q in union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ) assume q in (proj1 D) "/\" (proj2 D) ; ::_thesis: q in union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } then consider x, y being Element of L such that A8: q = x "/\" y and A9: x in proj1 D and A10: y in proj2 D by A1; reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5; ( not xx "/\" T is empty & xx "/\" T is directed ) ; then A11: {x} "/\" (proj2 D) in { X where X is non empty directed Subset of L : S1[X] } by A9; {x} "/\" (proj2 D) = { (x "/\" d) where d is Element of L : d in proj2 D } by YELLOW_4:42; then q in {x} "/\" (proj2 D) by A8, A10; hence q in union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } by A11, TARSKI:def_4; ::_thesis: verum end; theorem Th7: :: WAYBEL_2:7 for L being up-complete Semilattice for D being non empty directed Subset of [:L,L:] holds ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L proof let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L let D be non empty directed Subset of [:L,L:]; ::_thesis: ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22; set A = { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" D2 & x in D1 ) } ; union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" D2 & x in D1 ) } c= the carrier of L proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" D2 & x in D1 ) } or q in the carrier of L ) assume q in union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" D2 & x in D1 ) } ; ::_thesis: q in the carrier of L then consider r being set such that A1: q in r and A2: r in { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" D2 & x in D1 ) } by TARSKI:def_4; ex s being non empty directed Subset of L st ( r = s & ex x being Element of L st ( s = {x} "/\" D2 & x in D1 ) ) by A2; hence q in the carrier of L by A1; ::_thesis: verum end; then reconsider S = union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" D2 & x in D1 ) } as Subset of L ; S = D1 "/\" D2 by Th6; hence ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L by WAYBEL_0:75; ::_thesis: verum end; theorem Th8: :: WAYBEL_2:8 for L being up-complete Semilattice for D being non empty directed Subset of [:L,L:] holds ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L proof let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L let D be non empty directed Subset of [:L,L:]; ::_thesis: ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22; defpred S1[ set ] means ex x being Element of L st ( $1 = {x} "/\" D2 & x in D1 ); set A = { (sup X) where X is non empty directed Subset of L : S1[X] } ; { (sup X) where X is non empty directed Subset of L : S1[X] } c= the carrier of L proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (sup X) where X is non empty directed Subset of L : S1[X] } or q in the carrier of L ) assume q in { (sup X) where X is non empty directed Subset of L : S1[X] } ; ::_thesis: q in the carrier of L then ex X being non empty directed Subset of L st ( q = sup X & S1[X] ) ; hence q in the carrier of L ; ::_thesis: verum end; then reconsider A = { (sup X) where X is non empty directed Subset of L : S1[X] } as Subset of L ; set R = { X where X is non empty directed Subset of L : S1[X] } ; union { X where X is non empty directed Subset of L : S1[X] } c= the carrier of L proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in union { X where X is non empty directed Subset of L : S1[X] } or q in the carrier of L ) assume q in union { X where X is non empty directed Subset of L : S1[X] } ; ::_thesis: q in the carrier of L then consider r being set such that A1: q in r and A2: r in { X where X is non empty directed Subset of L : S1[X] } by TARSKI:def_4; ex s being non empty directed Subset of L st ( r = s & ex x being Element of L st ( s = {x} "/\" D2 & x in D1 ) ) by A2; hence q in the carrier of L by A1; ::_thesis: verum end; then reconsider UR = union { X where X is non empty directed Subset of L : S1[X] } as Subset of L ; set a = sup UR; A3: ex_sup_of UR,L by Th7; A4: for b being Element of L st A is_<=_than b holds sup UR <= b proof let b be Element of L; ::_thesis: ( A is_<=_than b implies sup UR <= b ) assume A5: A is_<=_than b ; ::_thesis: sup UR <= b UR is_<=_than b proof let k be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not k in UR or k <= b ) assume k in UR ; ::_thesis: k <= b then consider k1 being set such that A6: k in k1 and A7: k1 in { X where X is non empty directed Subset of L : S1[X] } by TARSKI:def_4; consider s being non empty directed Subset of L such that A8: k1 = s and A9: S1[s] by A7; consider x being Element of L such that A10: s = {x} "/\" D2 and x in D1 by A9; A11: {x} "/\" D2 = { (x "/\" d2) where d2 is Element of L : d2 in D2 } by YELLOW_4:42; sup s in A by A9; then A12: sup s <= b by A5, LATTICE3:def_9; consider d2 being Element of L such that A13: k = x "/\" d2 and d2 in D2 by A6, A8, A10, A11; x "/\" d2 <= sup s by A6, A8, A10, A13, Th1, YELLOW_4:1; hence k <= b by A13, A12, YELLOW_0:def_2; ::_thesis: verum end; hence sup UR <= b by A3, YELLOW_0:def_9; ::_thesis: verum end; A is_<=_than sup UR proof let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in A or b <= sup UR ) assume b in A ; ::_thesis: b <= sup UR then consider X being non empty directed Subset of L such that A14: b = sup X and A15: S1[X] ; ( ex_sup_of X,L & X in { X where X is non empty directed Subset of L : S1[X] } ) by A15, WAYBEL_0:75; hence b <= sup UR by A3, A14, YELLOW_0:34, ZFMISC_1:74; ::_thesis: verum end; hence ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L by A4, YELLOW_0:15; ::_thesis: verum end; theorem Th9: :: WAYBEL_2:9 for L being up-complete Semilattice for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L) proof let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L) let D be non empty directed Subset of [:L,L:]; ::_thesis: "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L) defpred S1[ set ] means ex x being Element of L st ( $1 = {x} "/\" (proj2 D) & x in proj1 D ); A1: "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) is_>=_than { (sup X) where X is non empty directed Subset of L : S1[X] } proof let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in { (sup X) where X is non empty directed Subset of L : S1[X] } or a <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) ) assume a in { (sup X) where X is non empty directed Subset of L : S1[X] } ; ::_thesis: a <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) then consider q being non empty directed Subset of L such that A2: a = sup q and A3: S1[q] ; A4: q in { X where X is non empty directed Subset of L : S1[X] } by A3; ( ex_sup_of q,L & ex_sup_of union { X where X is non empty directed Subset of L : S1[X] } ,L ) by Th7, WAYBEL_0:75; hence a <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) by A2, A4, YELLOW_0:34, ZFMISC_1:74; ::_thesis: verum end; ex_sup_of { (sup X) where X is non empty directed Subset of L : S1[X] } ,L by Th8; hence "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L) by A1, YELLOW_0:def_9; ::_thesis: verum end; theorem Th10: :: WAYBEL_2:10 for L being up-complete Semilattice for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L) proof let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L) let D be non empty directed Subset of [:L,L:]; ::_thesis: "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L) defpred S1[ set ] means ex x being Element of L st ( $1 = {x} "/\" (proj2 D) & x in proj1 D ); A1: "\/" ( { (sup X) where X is non empty directed Subset of L : S1[X] } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) by Th9; A2: union { X where X is non empty directed Subset of L : S1[X] } is_<=_than "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) proof let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in union { X where X is non empty directed Subset of L : S1[X] } or a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) ) assume a in union { X where X is non empty directed Subset of L : S1[X] } ; ::_thesis: a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) then consider b being set such that A3: a in b and A4: b in { X where X is non empty directed Subset of L : S1[X] } by TARSKI:def_4; consider c being non empty directed Subset of L such that A5: b = c and A6: S1[c] by A4; "\/" (c,L) in { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } by A6; then A7: "\/" (c,L) <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) by Th8, YELLOW_4:1; ex_sup_of c,L by WAYBEL_0:75; then a <= "\/" (c,L) by A3, A5, YELLOW_4:1; hence a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) by A7, YELLOW_0:def_2; ::_thesis: verum end; ex_sup_of union { X where X is non empty directed Subset of L : S1[X] } ,L by Th7; then "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) by A2, YELLOW_0:def_9; hence "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L) by A1, ORDERS_2:2; ::_thesis: verum end; registration let S, T be non empty reflexive up-complete RelStr ; cluster[:S,T:] -> up-complete ; coherence [:S,T:] is up-complete proof let X be non empty directed Subset of [:S,T:]; :: according to WAYBEL_0:def_39 ::_thesis: ex b1 being Element of the carrier of [:S,T:] st ( X is_<=_than b1 & ( for b2 being Element of the carrier of [:S,T:] holds ( not X is_<=_than b2 or b1 <= b2 ) ) ) reconsider X1 = proj1 X as non empty directed Subset of S by YELLOW_3:21, YELLOW_3:22; reconsider X2 = proj2 X as non empty directed Subset of T by YELLOW_3:21, YELLOW_3:22; consider x being Element of S such that A1: x is_>=_than X1 and A2: for z being Element of S st z is_>=_than X1 holds x <= z by WAYBEL_0:def_39; consider y being Element of T such that A3: y is_>=_than X2 and A4: for z being Element of T st z is_>=_than X2 holds y <= z by WAYBEL_0:def_39; take [x,y] ; ::_thesis: ( X is_<=_than [x,y] & ( for b1 being Element of the carrier of [:S,T:] holds ( not X is_<=_than b1 or [x,y] <= b1 ) ) ) thus [x,y] is_>=_than X by A1, A3, YELLOW_3:31; ::_thesis: for b1 being Element of the carrier of [:S,T:] holds ( not X is_<=_than b1 or [x,y] <= b1 ) let z be Element of [:S,T:]; ::_thesis: ( not X is_<=_than z or [x,y] <= z ) assume A5: z is_>=_than X ; ::_thesis: [x,y] <= z the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2; then A6: z = [(z `1),(z `2)] by MCART_1:21; then z `2 is_>=_than X2 by A5, YELLOW_3:31; then A7: y <= z `2 by A4; z `1 is_>=_than X1 by A5, A6, YELLOW_3:31; then x <= z `1 by A2; hence [x,y] <= z by A6, A7, YELLOW_3:11; ::_thesis: verum end; end; theorem :: WAYBEL_2:11 for S, T being non empty reflexive antisymmetric RelStr st [:S,T:] is up-complete holds ( S is up-complete & T is up-complete ) proof let S, T be non empty reflexive antisymmetric RelStr ; ::_thesis: ( [:S,T:] is up-complete implies ( S is up-complete & T is up-complete ) ) assume A1: [:S,T:] is up-complete ; ::_thesis: ( S is up-complete & T is up-complete ) thus S is up-complete ::_thesis: T is up-complete proof set D = the non empty directed Subset of T; let X be non empty directed Subset of S; :: according to WAYBEL_0:def_39 ::_thesis: ex b1 being Element of the carrier of S st ( X is_<=_than b1 & ( for b2 being Element of the carrier of S holds ( not X is_<=_than b2 or b1 <= b2 ) ) ) consider x being Element of [:S,T:] such that A2: x is_>=_than [:X, the non empty directed Subset of T:] and A3: for y being Element of [:S,T:] st y is_>=_than [:X, the non empty directed Subset of T:] holds x <= y by A1, WAYBEL_0:def_39; take x `1 ; ::_thesis: ( X is_<=_than x `1 & ( for b1 being Element of the carrier of S holds ( not X is_<=_than b1 or x `1 <= b1 ) ) ) the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2; then A4: x = [(x `1),(x `2)] by MCART_1:21; hence x `1 is_>=_than X by A2, YELLOW_3:29; ::_thesis: for b1 being Element of the carrier of S holds ( not X is_<=_than b1 or x `1 <= b1 ) ex_sup_of [:X, the non empty directed Subset of T:],[:S,T:] by A1, WAYBEL_0:75; then ex_sup_of the non empty directed Subset of T,T by YELLOW_3:39; then A5: sup the non empty directed Subset of T is_>=_than the non empty directed Subset of T by YELLOW_0:def_9; let y be Element of S; ::_thesis: ( not X is_<=_than y or x `1 <= y ) assume y is_>=_than X ; ::_thesis: x `1 <= y then x <= [y,(sup the non empty directed Subset of T)] by A3, A5, YELLOW_3:30; hence x `1 <= y by A4, YELLOW_3:11; ::_thesis: verum end; set D = the non empty directed Subset of S; let X be non empty directed Subset of T; :: according to WAYBEL_0:def_39 ::_thesis: ex b1 being Element of the carrier of T st ( X is_<=_than b1 & ( for b2 being Element of the carrier of T holds ( not X is_<=_than b2 or b1 <= b2 ) ) ) consider x being Element of [:S,T:] such that A6: x is_>=_than [: the non empty directed Subset of S,X:] and A7: for y being Element of [:S,T:] st y is_>=_than [: the non empty directed Subset of S,X:] holds x <= y by A1, WAYBEL_0:def_39; ex_sup_of [: the non empty directed Subset of S,X:],[:S,T:] by A1, WAYBEL_0:75; then ex_sup_of the non empty directed Subset of S,S by YELLOW_3:39; then A8: sup the non empty directed Subset of S is_>=_than the non empty directed Subset of S by YELLOW_0:def_9; take x `2 ; ::_thesis: ( X is_<=_than x `2 & ( for b1 being Element of the carrier of T holds ( not X is_<=_than b1 or x `2 <= b1 ) ) ) the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2; then A9: x = [(x `1),(x `2)] by MCART_1:21; hence x `2 is_>=_than X by A6, YELLOW_3:29; ::_thesis: for b1 being Element of the carrier of T holds ( not X is_<=_than b1 or x `2 <= b1 ) let y be Element of T; ::_thesis: ( not X is_<=_than y or x `2 <= y ) assume y is_>=_than X ; ::_thesis: x `2 <= y then x <= [(sup the non empty directed Subset of S),y] by A7, A8, YELLOW_3:30; hence x `2 <= y by A9, YELLOW_3:11; ::_thesis: verum end; theorem Th12: :: WAYBEL_2:12 for L being non empty reflexive antisymmetric up-complete RelStr for D being non empty directed Subset of [:L,L:] holds sup D = [(sup (proj1 D)),(sup (proj2 D))] proof let L be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for D being non empty directed Subset of [:L,L:] holds sup D = [(sup (proj1 D)),(sup (proj2 D))] let D be non empty directed Subset of [:L,L:]; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))] reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22; reconsider C = the carrier of L as non empty set ; reconsider D9 = D as non empty Subset of [:C,C:] by YELLOW_3:def_2; A1: ex_sup_of D1,L by WAYBEL_0:75; the carrier of [:L,L:] = [:C,C:] by YELLOW_3:def_2; then consider d1, d2 being set such that A2: ( d1 in C & d2 in C ) and A3: sup D = [d1,d2] by ZFMISC_1:def_2; A4: ex_sup_of D2,L by WAYBEL_0:75; reconsider d1 = d1, d2 = d2 as Element of L by A2; A5: ex_sup_of D,[:L,L:] by WAYBEL_0:75; D2 is_<=_than d2 proof let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in D2 or b <= d2 ) assume b in D2 ; ::_thesis: b <= d2 then consider x being set such that A6: [x,b] in D by XTUPLE_0:def_13; reconsider x = x as Element of D1 by A6, XTUPLE_0:def_12; D is_<=_than [d1,d2] by A5, A3, YELLOW_0:def_9; then [x,b] <= [d1,d2] by A6, LATTICE3:def_9; hence b <= d2 by YELLOW_3:11; ::_thesis: verum end; then A7: sup D2 <= d2 by A4, YELLOW_0:def_9; D1 is_<=_than d1 proof let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in D1 or b <= d1 ) assume b in D1 ; ::_thesis: b <= d1 then consider x being set such that A8: [b,x] in D by XTUPLE_0:def_12; reconsider x = x as Element of D2 by A8, XTUPLE_0:def_13; D is_<=_than [d1,d2] by A5, A3, YELLOW_0:def_9; then [b,x] <= [d1,d2] by A8, LATTICE3:def_9; hence b <= d1 by YELLOW_3:11; ::_thesis: verum end; then sup D1 <= d1 by A1, YELLOW_0:def_9; then A9: [(sup D1),(sup D2)] <= sup D by A3, A7, YELLOW_3:11; A10: ex_sup_of [:D1,D2:],[:L,L:] by WAYBEL_0:75; reconsider D1 = D1, D2 = D2 as non empty Subset of L ; D9 c= [:D1,D2:] by YELLOW_3:1; then sup D <= sup [:D1,D2:] by A5, A10, YELLOW_0:34; then sup D <= [(sup (proj1 D)),(sup (proj2 D))] by A1, A4, YELLOW_3:43; hence sup D = [(sup (proj1 D)),(sup (proj2 D))] by A9, ORDERS_2:2; ::_thesis: verum end; theorem Th13: :: WAYBEL_2:13 for S1, S2 being RelStr for D being Subset of S1 for f being Function of S1,S2 st f is monotone holds f .: (downarrow D) c= downarrow (f .: D) proof let S1, S2 be RelStr ; ::_thesis: for D being Subset of S1 for f being Function of S1,S2 st f is monotone holds f .: (downarrow D) c= downarrow (f .: D) let D be Subset of S1; ::_thesis: for f being Function of S1,S2 st f is monotone holds f .: (downarrow D) c= downarrow (f .: D) let f be Function of S1,S2; ::_thesis: ( f is monotone implies f .: (downarrow D) c= downarrow (f .: D) ) assume A1: f is monotone ; ::_thesis: f .: (downarrow D) c= downarrow (f .: D) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in f .: (downarrow D) or q in downarrow (f .: D) ) assume A2: q in f .: (downarrow D) ; ::_thesis: q in downarrow (f .: D) then consider x being set such that A3: x in dom f and A4: x in downarrow D and A5: q = f . x by FUNCT_1:def_6; reconsider s1 = S1, s2 = S2 as non empty RelStr by A2; reconsider x = x as Element of s1 by A3; consider y being Element of s1 such that A6: x <= y and A7: y in D by A4, WAYBEL_0:def_15; reconsider f1 = f as Function of s1,s2 ; f1 . x is Element of s2 ; then reconsider q1 = q, fy = f1 . y as Element of s2 by A5; the carrier of s2 <> {} ; then dom f = the carrier of s1 by FUNCT_2:def_1; then A8: f . y in f .: D by A7, FUNCT_1:def_6; q1 <= fy by A1, A5, A6, ORDERS_3:def_5; hence q in downarrow (f .: D) by A8, WAYBEL_0:def_15; ::_thesis: verum end; theorem Th14: :: WAYBEL_2:14 for S1, S2 being RelStr for D being Subset of S1 for f being Function of S1,S2 st f is monotone holds f .: (uparrow D) c= uparrow (f .: D) proof let S1, S2 be RelStr ; ::_thesis: for D being Subset of S1 for f being Function of S1,S2 st f is monotone holds f .: (uparrow D) c= uparrow (f .: D) let D be Subset of S1; ::_thesis: for f being Function of S1,S2 st f is monotone holds f .: (uparrow D) c= uparrow (f .: D) let f be Function of S1,S2; ::_thesis: ( f is monotone implies f .: (uparrow D) c= uparrow (f .: D) ) assume A1: f is monotone ; ::_thesis: f .: (uparrow D) c= uparrow (f .: D) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in f .: (uparrow D) or q in uparrow (f .: D) ) assume A2: q in f .: (uparrow D) ; ::_thesis: q in uparrow (f .: D) then consider x being set such that A3: x in dom f and A4: x in uparrow D and A5: q = f . x by FUNCT_1:def_6; reconsider s1 = S1, s2 = S2 as non empty RelStr by A2; reconsider x = x as Element of s1 by A3; consider y being Element of s1 such that A6: y <= x and A7: y in D by A4, WAYBEL_0:def_16; reconsider f1 = f as Function of s1,s2 ; f1 . x is Element of s2 ; then reconsider q1 = q, fy = f1 . y as Element of s2 by A5; the carrier of s2 <> {} ; then dom f = the carrier of s1 by FUNCT_2:def_1; then A8: f . y in f .: D by A7, FUNCT_1:def_6; fy <= q1 by A1, A5, A6, ORDERS_3:def_5; hence q in uparrow (f .: D) by A8, WAYBEL_0:def_16; ::_thesis: verum end; registration cluster1 -element reflexive -> 1 -element reflexive distributive complemented for RelStr ; coherence for b1 being 1 -element reflexive RelStr holds ( b1 is distributive & b1 is complemented ) proof let L be 1 -element reflexive RelStr ; ::_thesis: ( L is distributive & L is complemented ) thus L is distributive ::_thesis: L is complemented proof let x, y, z be Element of L; :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) thus x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by STRUCT_0:def_10; ::_thesis: verum end; let x be Element of L; :: according to WAYBEL_1:def_24 ::_thesis: ex b1 being Element of the carrier of L st b1 is_a_complement_of x take y = x; ::_thesis: y is_a_complement_of x thus x "\/" y = Top L by STRUCT_0:def_10; :: according to WAYBEL_1:def_23 ::_thesis: x "/\" y = Bottom L thus x "/\" y = Bottom L by STRUCT_0:def_10; ::_thesis: verum end; end; registration cluster non empty 1 -element strict V70() reflexive transitive antisymmetric non void with_suprema with_infima for RelStr ; existence ex b1 being LATTICE st ( b1 is strict & b1 is 1 -element ) proof set B = the 1 -element strict reflexive RelStr ; take the 1 -element strict reflexive RelStr ; ::_thesis: ( the 1 -element strict reflexive RelStr is strict & the 1 -element strict reflexive RelStr is 1 -element ) thus ( the 1 -element strict reflexive RelStr is strict & the 1 -element strict reflexive RelStr is 1 -element ) ; ::_thesis: verum end; end; theorem Th15: :: WAYBEL_2:15 for H being distributive complete LATTICE for a being Element of H for X being finite Subset of H holds sup ({a} "/\" X) = a "/\" (sup X) proof let H be distributive complete LATTICE; ::_thesis: for a being Element of H for X being finite Subset of H holds sup ({a} "/\" X) = a "/\" (sup X) let a be Element of H; ::_thesis: for X being finite Subset of H holds sup ({a} "/\" X) = a "/\" (sup X) let X be finite Subset of H; ::_thesis: sup ({a} "/\" X) = a "/\" (sup X) defpred S1[ set ] means ex A being Subset of H st ( A = $1 & a "/\" (sup A) = sup ({a} "/\" A) ); A1: S1[ {} ] proof reconsider A = {} as Subset of H by XBOOLE_1:2; take A ; ::_thesis: ( A = {} & a "/\" (sup A) = sup ({a} "/\" A) ) thus A = {} ; ::_thesis: a "/\" (sup A) = sup ({a} "/\" A) ( Bottom H <= a & {a} "/\" ({} H) = {} ) by YELLOW_0:44, YELLOW_4:36; hence a "/\" (sup A) = sup ({a} "/\" A) by YELLOW_0:25; ::_thesis: verum end; A2: for x, B being set st x in X & B c= X & S1[B] holds S1[B \/ {x}] proof let x, B be set ; ::_thesis: ( x in X & B c= X & S1[B] implies S1[B \/ {x}] ) assume that A3: x in X and A4: B c= X and A5: S1[B] ; ::_thesis: S1[B \/ {x}] reconsider x1 = x as Element of H by A3; A6: {x1} c= the carrier of H ; B c= the carrier of H by A4, XBOOLE_1:1; then reconsider C = B \/ {x} as Subset of H by A6, XBOOLE_1:8; take C ; ::_thesis: ( C = B \/ {x} & a "/\" (sup C) = sup ({a} "/\" C) ) thus C = B \/ {x} ; ::_thesis: a "/\" (sup C) = sup ({a} "/\" C) consider A being Subset of H such that A7: A = B and A8: a "/\" (sup A) = sup ({a} "/\" A) by A5; A9: {a} "/\" C = ({a} "/\" A) \/ ({a} "/\" {x1}) by A7, YELLOW_4:43 .= ({a} "/\" A) \/ {(a "/\" x1)} by YELLOW_4:46 ; A10: ( ex_sup_of {a} "/\" A,H & ex_sup_of {(a "/\" x1)},H ) by YELLOW_0:17; ( ex_sup_of B,H & ex_sup_of {x},H ) by YELLOW_0:17; hence a "/\" (sup C) = a "/\" (("\/" (B,H)) "\/" ("\/" ({x},H))) by YELLOW_2:3 .= (sup ({a} "/\" A)) "\/" (a "/\" ("\/" ({x},H))) by A7, A8, WAYBEL_1:def_3 .= (sup ({a} "/\" A)) "\/" (a "/\" x1) by YELLOW_0:39 .= (sup ({a} "/\" A)) "\/" (sup {(a "/\" x1)}) by YELLOW_0:39 .= sup ({a} "/\" C) by A10, A9, YELLOW_2:3 ; ::_thesis: verum end; A11: X is finite ; S1[X] from FINSET_1:sch_2(A11, A1, A2); hence sup ({a} "/\" X) = a "/\" (sup X) ; ::_thesis: verum end; theorem :: WAYBEL_2:16 for H being distributive complete LATTICE for a being Element of H for X being finite Subset of H holds inf ({a} "\/" X) = a "\/" (inf X) proof let H be distributive complete LATTICE; ::_thesis: for a being Element of H for X being finite Subset of H holds inf ({a} "\/" X) = a "\/" (inf X) let a be Element of H; ::_thesis: for X being finite Subset of H holds inf ({a} "\/" X) = a "\/" (inf X) let X be finite Subset of H; ::_thesis: inf ({a} "\/" X) = a "\/" (inf X) defpred S1[ set ] means ex A being Subset of H st ( A = $1 & a "\/" (inf A) = inf ({a} "\/" A) ); A1: S1[ {} ] proof reconsider A = {} as Subset of H by XBOOLE_1:2; take A ; ::_thesis: ( A = {} & a "\/" (inf A) = inf ({a} "\/" A) ) thus A = {} ; ::_thesis: a "\/" (inf A) = inf ({a} "\/" A) ( a <= Top H & {a} "\/" ({} H) = {} ) by YELLOW_0:45, YELLOW_4:9; hence a "\/" (inf A) = inf ({a} "\/" A) by YELLOW_0:24; ::_thesis: verum end; A2: for x, B being set st x in X & B c= X & S1[B] holds S1[B \/ {x}] proof let x, B be set ; ::_thesis: ( x in X & B c= X & S1[B] implies S1[B \/ {x}] ) assume that A3: x in X and A4: B c= X and A5: S1[B] ; ::_thesis: S1[B \/ {x}] reconsider x1 = x as Element of H by A3; A6: {x1} c= the carrier of H ; B c= the carrier of H by A4, XBOOLE_1:1; then reconsider C = B \/ {x} as Subset of H by A6, XBOOLE_1:8; take C ; ::_thesis: ( C = B \/ {x} & a "\/" (inf C) = inf ({a} "\/" C) ) thus C = B \/ {x} ; ::_thesis: a "\/" (inf C) = inf ({a} "\/" C) consider A being Subset of H such that A7: A = B and A8: a "\/" (inf A) = inf ({a} "\/" A) by A5; A9: {a} "\/" C = ({a} "\/" A) \/ ({a} "\/" {x1}) by A7, YELLOW_4:16 .= ({a} "\/" A) \/ {(a "\/" x1)} by YELLOW_4:19 ; A10: ( ex_inf_of {a} "\/" A,H & ex_inf_of {(a "\/" x1)},H ) by YELLOW_0:17; ( ex_inf_of B,H & ex_inf_of {x},H ) by YELLOW_0:17; hence a "\/" (inf C) = a "\/" (("/\" (B,H)) "/\" ("/\" ({x},H))) by YELLOW_2:4 .= (inf ({a} "\/" A)) "/\" (a "\/" ("/\" ({x},H))) by A7, A8, WAYBEL_1:5 .= (inf ({a} "\/" A)) "/\" (a "\/" x1) by YELLOW_0:39 .= (inf ({a} "\/" A)) "/\" (inf {(a "\/" x1)}) by YELLOW_0:39 .= inf ({a} "\/" C) by A10, A9, YELLOW_2:4 ; ::_thesis: verum end; A11: X is finite ; S1[X] from FINSET_1:sch_2(A11, A1, A2); hence inf ({a} "\/" X) = a "\/" (inf X) ; ::_thesis: verum end; theorem Th17: :: WAYBEL_2:17 for H being distributive complete LATTICE for a being Element of H for X being finite Subset of H holds a "/\" preserves_sup_of X proof let H be distributive complete LATTICE; ::_thesis: for a being Element of H for X being finite Subset of H holds a "/\" preserves_sup_of X let a be Element of H; ::_thesis: for X being finite Subset of H holds a "/\" preserves_sup_of X let X be finite Subset of H; ::_thesis: a "/\" preserves_sup_of X assume ex_sup_of X,H ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (a "/\") .: X,H & "\/" (((a "/\") .: X),H) = (a "/\") . ("\/" (X,H)) ) thus ex_sup_of (a "/\") .: X,H by YELLOW_0:17; ::_thesis: "\/" (((a "/\") .: X),H) = (a "/\") . ("\/" (X,H)) thus sup ((a "/\") .: X) = "\/" ( { (a "/\" y) where y is Element of H : y in X } ,H) by WAYBEL_1:61 .= sup ({a} "/\" X) by YELLOW_4:42 .= a "/\" (sup X) by Th15 .= (a "/\") . (sup X) by WAYBEL_1:def_18 ; ::_thesis: verum end; begin scheme :: WAYBEL_2:sch 1 ExNet{ F1() -> non empty RelStr , F2() -> prenet of F1(), F3( set ) -> Element of F1() } : ex M being prenet of F1() st ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) & ( for i being Element of M holds the mapping of M . i = F3(( the mapping of F2() . i)) ) ) proof deffunc H1( Element of F2()) -> Element of F1() = F3(( the mapping of F2() . $1)); A1: for i being Element of F2() holds H1(i) in the carrier of F1() ; consider f being Function of the carrier of F2(), the carrier of F1() such that A2: for i being Element of F2() holds f . i = H1(i) from FUNCT_2:sch_8(A1); set M = NetStr(# the carrier of F2(), the InternalRel of F2(),f #); ( RelStr(# the carrier of NetStr(# the carrier of F2(), the InternalRel of F2(),f #), the InternalRel of NetStr(# the carrier of F2(), the InternalRel of F2(),f #) #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) & [#] F2() is directed ) by WAYBEL_0:def_6; then [#] NetStr(# the carrier of F2(), the InternalRel of F2(),f #) is directed by WAYBEL_0:3; then reconsider M = NetStr(# the carrier of F2(), the InternalRel of F2(),f #) as prenet of F1() by WAYBEL_0:def_6; take M ; ::_thesis: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) & ( for i being Element of M holds the mapping of M . i = F3(( the mapping of F2() . i)) ) ) thus ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) & ( for i being Element of M holds the mapping of M . i = F3(( the mapping of F2() . i)) ) ) by A2; ::_thesis: verum end; theorem Th18: :: WAYBEL_2:18 for L being non empty RelStr for N being prenet of L st N is eventually-directed holds rng (netmap (N,L)) is directed proof let L be non empty RelStr ; ::_thesis: for N being prenet of L st N is eventually-directed holds rng (netmap (N,L)) is directed let N be prenet of L; ::_thesis: ( N is eventually-directed implies rng (netmap (N,L)) is directed ) assume A1: N is eventually-directed ; ::_thesis: rng (netmap (N,L)) is directed set f = netmap (N,L); let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in rng (netmap (N,L)) or not y in rng (netmap (N,L)) or ex b1 being Element of the carrier of L st ( b1 in rng (netmap (N,L)) & x <= b1 & y <= b1 ) ) assume that A2: x in rng (netmap (N,L)) and A3: y in rng (netmap (N,L)) ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in rng (netmap (N,L)) & x <= b1 & y <= b1 ) consider a being set such that A4: a in dom (netmap (N,L)) and A5: (netmap (N,L)) . a = x by A2, FUNCT_1:def_3; consider b being set such that A6: b in dom (netmap (N,L)) and A7: (netmap (N,L)) . b = y by A3, FUNCT_1:def_3; reconsider a = a, b = b as Element of N by A4, A6; consider ja being Element of N such that A8: for k being Element of N st ja <= k holds N . a <= N . k by A1, WAYBEL_0:11; consider jb being Element of N such that A9: for k being Element of N st jb <= k holds N . b <= N . k by A1, WAYBEL_0:11; [#] N is directed by WAYBEL_0:def_6; then consider c being Element of N such that c in [#] N and A10: ( ja <= c & jb <= c ) by WAYBEL_0:def_1; take z = (netmap (N,L)) . c; ::_thesis: ( z in rng (netmap (N,L)) & x <= z & y <= z ) dom (netmap (N,L)) = the carrier of N by FUNCT_2:def_1; hence z in rng (netmap (N,L)) by FUNCT_1:def_3; ::_thesis: ( x <= z & y <= z ) N . c = (netmap (N,L)) . c ; hence ( x <= z & y <= z ) by A5, A7, A8, A9, A10; ::_thesis: verum end; theorem Th19: :: WAYBEL_2:19 for L being non empty reflexive RelStr for D being non empty directed Subset of L for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L proof let L be non empty reflexive RelStr ; ::_thesis: for D being non empty directed Subset of L for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L let D be non empty directed Subset of L; ::_thesis: for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L let n be Function of D, the carrier of L; ::_thesis: NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L set N = NetStr(# D,( the InternalRel of L |_2 D),n #); NetStr(# D,( the InternalRel of L |_2 D),n #) is directed proof let x, y be Element of NetStr(# D,( the InternalRel of L |_2 D),n #); :: according to WAYBEL_0:def_1,WAYBEL_0:def_6 ::_thesis: ( not x in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) or not y in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) or ex b1 being Element of the carrier of NetStr(# D,( the InternalRel of L |_2 D),n #) st ( b1 in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) & x <= b1 & y <= b1 ) ) assume that x in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) and y in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) ; ::_thesis: ex b1 being Element of the carrier of NetStr(# D,( the InternalRel of L |_2 D),n #) st ( b1 in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) & x <= b1 & y <= b1 ) reconsider x1 = x, y1 = y as Element of D ; consider z1 being Element of L such that A1: z1 in D and A2: ( x1 <= z1 & y1 <= z1 ) by WAYBEL_0:def_1; reconsider z = z1 as Element of NetStr(# D,( the InternalRel of L |_2 D),n #) by A1; take z ; ::_thesis: ( z in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) & x <= z & y <= z ) thus z in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) ; ::_thesis: ( x <= z & y <= z ) the InternalRel of NetStr(# D,( the InternalRel of L |_2 D),n #) c= the InternalRel of L by XBOOLE_1:17; then reconsider N = NetStr(# D,( the InternalRel of L |_2 D),n #) as SubRelStr of L by YELLOW_0:def_13; N is full by YELLOW_0:def_14; hence ( x <= z & y <= z ) by A2, YELLOW_0:60; ::_thesis: verum end; hence NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L ; ::_thesis: verum end; theorem Th20: :: WAYBEL_2:20 for L being non empty reflexive RelStr for D being non empty directed Subset of L for n being Function of D, the carrier of L for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds N is eventually-directed proof let L be non empty reflexive RelStr ; ::_thesis: for D being non empty directed Subset of L for n being Function of D, the carrier of L for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds N is eventually-directed let D be non empty directed Subset of L; ::_thesis: for n being Function of D, the carrier of L for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds N is eventually-directed let n be Function of D, the carrier of L; ::_thesis: for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds N is eventually-directed let N be prenet of L; ::_thesis: ( n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) implies N is eventually-directed ) assume that A1: n = id D and A2: N = NetStr(# D,( the InternalRel of L |_2 D),n #) ; ::_thesis: N is eventually-directed for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i <= N . k proof let i be Element of N; ::_thesis: ex j being Element of N st for k being Element of N st j <= k holds N . i <= N . k take j = i; ::_thesis: for k being Element of N st j <= k holds N . i <= N . k let k be Element of N; ::_thesis: ( j <= k implies N . i <= N . k ) assume A3: j <= k ; ::_thesis: N . i <= N . k the InternalRel of N c= the InternalRel of L by A2, XBOOLE_1:17; then A4: N is SubRelStr of L by A2, YELLOW_0:def_13; reconsider nj = n . j, nk = n . k as Element of L by A2, FUNCT_2:5; ( nj = j & nk = k ) by A1, A2, FUNCT_1:18; hence N . i <= N . k by A2, A3, A4, YELLOW_0:59; ::_thesis: verum end; hence N is eventually-directed by WAYBEL_0:11; ::_thesis: verum end; definition let L be non empty RelStr ; let N be NetStr over L; func sup N -> Element of L equals :: WAYBEL_2:def 1 Sup ; coherence Sup is Element of L ; end; :: deftheorem defines sup WAYBEL_2:def_1_:_ for L being non empty RelStr for N being NetStr over L holds sup N = Sup ; definition let L be non empty RelStr ; let J be set ; let f be Function of J, the carrier of L; func FinSups f -> prenet of L means :Def2: :: WAYBEL_2:def 2 ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & it = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ); existence ex b1 being prenet of L ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) proof deffunc H1( Element of Fin J) -> Element of the carrier of L = sup (f .: $1); A1: for x being Element of Fin J holds H1(x) in the carrier of L ; consider g being Function of (Fin J), the carrier of L such that A2: for x being Element of Fin J holds g . x = H1(x) from FUNCT_2:sch_8(A1); set M = NetStr(# (Fin J),(RelIncl (Fin J)),g #); NetStr(# (Fin J),(RelIncl (Fin J)),g #) is directed proof let x, y be Element of NetStr(# (Fin J),(RelIncl (Fin J)),g #); :: according to WAYBEL_0:def_1,WAYBEL_0:def_6 ::_thesis: ( not x in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) or not y in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) or ex b1 being Element of the carrier of NetStr(# (Fin J),(RelIncl (Fin J)),g #) st ( b1 in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) & x <= b1 & y <= b1 ) ) assume that x in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) and y in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) ; ::_thesis: ex b1 being Element of the carrier of NetStr(# (Fin J),(RelIncl (Fin J)),g #) st ( b1 in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) & x <= b1 & y <= b1 ) reconsider x1 = x, y1 = y as Element of Fin J ; reconsider z = x1 \/ y1 as Element of NetStr(# (Fin J),(RelIncl (Fin J)),g #) ; take z ; ::_thesis: ( z in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) & x <= z & y <= z ) thus z in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) ; ::_thesis: ( x <= z & y <= z ) A3: InclPoset (Fin J) = RelStr(# (Fin J),(RelIncl (Fin J)) #) by YELLOW_1:def_1; then reconsider x2 = x, y2 = y, z1 = z as Element of (InclPoset (Fin J)) ; y c= z by XBOOLE_1:7; then A4: y2 <= z1 by YELLOW_1:3; x c= z by XBOOLE_1:7; then x2 <= z1 by YELLOW_1:3; hence ( x <= z & y <= z ) by A3, A4, YELLOW_0:1; ::_thesis: verum end; then reconsider M = NetStr(# (Fin J),(RelIncl (Fin J)),g #) as prenet of L ; take M ; ::_thesis: ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & M = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) thus ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & M = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being prenet of L st ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & b2 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) holds b1 = b2 proof let A, B be prenet of L; ::_thesis: ( ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) implies A = B ) assume that A5: ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) and A6: ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) ; ::_thesis: A = B consider g1 being Function of (Fin J), the carrier of L such that A7: for x being Element of Fin J holds ( g1 . x = sup (f .: x) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g1 #) ) by A5; consider g2 being Function of (Fin J), the carrier of L such that A8: for x being Element of Fin J holds ( g2 . x = sup (f .: x) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g2 #) ) by A6; for x being set st x in Fin J holds g1 . x = g2 . x proof let x be set ; ::_thesis: ( x in Fin J implies g1 . x = g2 . x ) assume A9: x in Fin J ; ::_thesis: g1 . x = g2 . x hence g1 . x = sup (f .: x) by A7 .= g2 . x by A8, A9 ; ::_thesis: verum end; hence A = B by A7, A8, FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def2 defines FinSups WAYBEL_2:def_2_:_ for L being non empty RelStr for J being set for f being Function of J, the carrier of L for b4 being prenet of L holds ( b4 = FinSups f iff ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & b4 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) ); theorem :: WAYBEL_2:21 for L being non empty RelStr for J, x being set for f being Function of J, the carrier of L holds ( x is Element of (FinSups f) iff x is Element of Fin J ) proof let L be non empty RelStr ; ::_thesis: for J, x being set for f being Function of J, the carrier of L holds ( x is Element of (FinSups f) iff x is Element of Fin J ) let J, x be set ; ::_thesis: for f being Function of J, the carrier of L holds ( x is Element of (FinSups f) iff x is Element of Fin J ) let f be Function of J, the carrier of L; ::_thesis: ( x is Element of (FinSups f) iff x is Element of Fin J ) ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2; hence ( x is Element of (FinSups f) iff x is Element of Fin J ) ; ::_thesis: verum end; registration let L be non empty reflexive antisymmetric complete RelStr ; let J be set ; let f be Function of J, the carrier of L; cluster FinSups f -> monotone ; coherence FinSups f is monotone proof let x, y be Element of (FinSups f); :: according to ORDERS_3:def_5,WAYBEL_0:def_9 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds ( not b1 = (netmap ((FinSups f),L)) . x or not b2 = (netmap ((FinSups f),L)) . y or b1 <= b2 ) ) assume A1: x <= y ; ::_thesis: for b1, b2 being Element of the carrier of L holds ( not b1 = (netmap ((FinSups f),L)) . x or not b2 = (netmap ((FinSups f),L)) . y or b1 <= b2 ) consider g being Function of (Fin J), the carrier of L such that A2: for x being Element of Fin J holds ( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2; g . x = sup (f .: x) by A2; then reconsider fx = g . x as Element of L ; A3: InclPoset (Fin J) = RelStr(# (Fin J),(RelIncl (Fin J)) #) by YELLOW_1:def_1; then reconsider x1 = x, y1 = y as Element of (InclPoset (Fin J)) by A2; A4: ( ex_sup_of f .: x,L & ex_sup_of f .: y,L ) by YELLOW_0:17; x1 <= y1 by A1, A2, A3, YELLOW_0:1; then x c= y by YELLOW_1:3; then sup (f .: x) <= sup (f .: y) by A4, RELAT_1:123, YELLOW_0:34; then A5: fx <= sup (f .: y) by A2; let a, b be Element of L; ::_thesis: ( not a = (netmap ((FinSups f),L)) . x or not b = (netmap ((FinSups f),L)) . y or a <= b ) assume ( a = (netmap ((FinSups f),L)) . x & b = (netmap ((FinSups f),L)) . y ) ; ::_thesis: a <= b hence a <= b by A2, A5; ::_thesis: verum end; end; definition let L be non empty RelStr ; let x be Element of L; let N be non empty NetStr over L; funcx "/\" N -> strict NetStr over L means :Def3: :: WAYBEL_2:def 3 ( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of it ex y being Element of L st ( y = the mapping of N . i & the mapping of it . i = x "/\" y ) ) ); existence ex b1 being strict NetStr over L st ( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b1 ex y being Element of L st ( y = the mapping of N . i & the mapping of b1 . i = x "/\" y ) ) ) proof defpred S1[ set , set ] means ex y being Element of L st ( y = the mapping of N . $1 & $2 = x "/\" y ); A1: for e being Element of N ex u being Element of L st S1[e,u] proof let e be Element of N; ::_thesis: ex u being Element of L st S1[e,u] take x "/\" ( the mapping of N . e) ; ::_thesis: S1[e,x "/\" ( the mapping of N . e)] take the mapping of N . e ; ::_thesis: ( the mapping of N . e = the mapping of N . e & x "/\" ( the mapping of N . e) = x "/\" ( the mapping of N . e) ) thus ( the mapping of N . e = the mapping of N . e & x "/\" ( the mapping of N . e) = x "/\" ( the mapping of N . e) ) ; ::_thesis: verum end; ex g being Function of the carrier of N, the carrier of L st for i being Element of N holds S1[i,g . i] from FUNCT_2:sch_3(A1); then consider g being Function of the carrier of N, the carrier of L such that A2: for i being Element of N ex y being Element of L st ( y = the mapping of N . i & g . i = x "/\" y ) ; take NetStr(# the carrier of N, the InternalRel of N,g #) ; ::_thesis: ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,g #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,g #) #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of NetStr(# the carrier of N, the InternalRel of N,g #) ex y being Element of L st ( y = the mapping of N . i & the mapping of NetStr(# the carrier of N, the InternalRel of N,g #) . i = x "/\" y ) ) ) thus ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,g #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,g #) #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of NetStr(# the carrier of N, the InternalRel of N,g #) ex y being Element of L st ( y = the mapping of N . i & the mapping of NetStr(# the carrier of N, the InternalRel of N,g #) . i = x "/\" y ) ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being strict NetStr over L st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b1 ex y being Element of L st ( y = the mapping of N . i & the mapping of b1 . i = x "/\" y ) ) & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b2 ex y being Element of L st ( y = the mapping of N . i & the mapping of b2 . i = x "/\" y ) ) holds b1 = b2 proof let A, B be strict NetStr over L; ::_thesis: ( RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of A ex y being Element of L st ( y = the mapping of N . i & the mapping of A . i = x "/\" y ) ) & RelStr(# the carrier of B, the InternalRel of B #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of B ex y being Element of L st ( y = the mapping of N . i & the mapping of B . i = x "/\" y ) ) implies A = B ) assume that A3: RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) and A4: for i being Element of A ex y being Element of L st ( y = the mapping of N . i & the mapping of A . i = x "/\" y ) and A5: RelStr(# the carrier of B, the InternalRel of B #) = RelStr(# the carrier of N, the InternalRel of N #) and A6: for i being Element of B ex y being Element of L st ( y = the mapping of N . i & the mapping of B . i = x "/\" y ) ; ::_thesis: A = B reconsider C = the carrier of A as non empty set by A3; reconsider f1 = the mapping of A, f2 = the mapping of B as Function of C, the carrier of L by A3, A5; for c being Element of C holds f1 . c = f2 . c proof let c be Element of C; ::_thesis: f1 . c = f2 . c ( ex ya being Element of L st ( ya = the mapping of N . c & f1 . c = x "/\" ya ) & ex yb being Element of L st ( yb = the mapping of N . c & f2 . c = x "/\" yb ) ) by A3, A4, A5, A6; hence f1 . c = f2 . c ; ::_thesis: verum end; hence A = B by A3, A5, FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def3 defines "/\" WAYBEL_2:def_3_:_ for L being non empty RelStr for x being Element of L for N being non empty NetStr over L for b4 being strict NetStr over L holds ( b4 = x "/\" N iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b4 ex y being Element of L st ( y = the mapping of N . i & the mapping of b4 . i = x "/\" y ) ) ) ); theorem Th22: :: WAYBEL_2:22 for L being non empty RelStr for N being non empty NetStr over L for x being Element of L for y being set holds ( y is Element of N iff y is Element of (x "/\" N) ) proof let L be non empty RelStr ; ::_thesis: for N being non empty NetStr over L for x being Element of L for y being set holds ( y is Element of N iff y is Element of (x "/\" N) ) let N be non empty NetStr over L; ::_thesis: for x being Element of L for y being set holds ( y is Element of N iff y is Element of (x "/\" N) ) let x be Element of L; ::_thesis: for y being set holds ( y is Element of N iff y is Element of (x "/\" N) ) let y be set ; ::_thesis: ( y is Element of N iff y is Element of (x "/\" N) ) RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def3; hence ( y is Element of N iff y is Element of (x "/\" N) ) ; ::_thesis: verum end; registration let L be non empty RelStr ; let x be Element of L; let N be non empty NetStr over L; clusterx "/\" N -> non empty strict ; coherence not x "/\" N is empty proof RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def3; hence not x "/\" N is empty ; ::_thesis: verum end; end; registration let L be non empty RelStr ; let x be Element of L; let N be prenet of L; clusterx "/\" N -> strict directed ; coherence x "/\" N is directed proof ( RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) & [#] N is directed ) by Def3, WAYBEL_0:def_6; hence [#] (x "/\" N) is directed by WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum end; end; theorem Th23: :: WAYBEL_2:23 for L being non empty RelStr for x being Element of L for F being non empty NetStr over L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F) proof let L be non empty RelStr ; ::_thesis: for x being Element of L for F being non empty NetStr over L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F) let x be Element of L; ::_thesis: for F being non empty NetStr over L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F) let F be non empty NetStr over L; ::_thesis: rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F) set f = the mapping of F; set h = the mapping of (x "/\" F); set A = rng the mapping of F; A1: {x} "/\" (rng the mapping of F) = { (x "/\" y) where y is Element of L : y in rng the mapping of F } by YELLOW_4:42; A2: RelStr(# the carrier of (x "/\" F), the InternalRel of (x "/\" F) #) = RelStr(# the carrier of F, the InternalRel of F #) by Def3; then A3: dom the mapping of (x "/\" F) = the carrier of F by FUNCT_2:def_1; A4: dom the mapping of F = the carrier of F by FUNCT_2:def_1; thus rng the mapping of (x "/\" F) c= {x} "/\" (rng the mapping of F) :: according to XBOOLE_0:def_10 ::_thesis: {x} "/\" (rng the mapping of F) c= rng the mapping of (x "/\" F) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng the mapping of (x "/\" F) or q in {x} "/\" (rng the mapping of F) ) assume q in rng the mapping of (x "/\" F) ; ::_thesis: q in {x} "/\" (rng the mapping of F) then consider a being set such that A5: a in dom the mapping of (x "/\" F) and A6: q = the mapping of (x "/\" F) . a by FUNCT_1:def_3; reconsider a = a as Element of (x "/\" F) by A5; consider y being Element of L such that A7: y = the mapping of F . a and A8: the mapping of (x "/\" F) . a = x "/\" y by Def3; y in rng the mapping of F by A2, A4, A7, FUNCT_1:def_3; hence q in {x} "/\" (rng the mapping of F) by A1, A6, A8; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "/\" (rng the mapping of F) or q in rng the mapping of (x "/\" F) ) assume q in {x} "/\" (rng the mapping of F) ; ::_thesis: q in rng the mapping of (x "/\" F) then consider y being Element of L such that A9: q = x "/\" y and A10: y in rng the mapping of F by A1; consider z being set such that A11: z in dom the mapping of F and A12: y = the mapping of F . z by A10, FUNCT_1:def_3; reconsider z = z as Element of (x "/\" F) by A2, A11; ex w being Element of L st ( w = the mapping of F . z & the mapping of (x "/\" F) . z = x "/\" w ) by Def3; hence q in rng the mapping of (x "/\" F) by A3, A9, A11, A12, FUNCT_1:def_3; ::_thesis: verum end; theorem Th24: :: WAYBEL_2:24 for L being non empty RelStr for J being set for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds rng (netmap ((FinSups f),L)) c= finsups (rng f) proof let L be non empty RelStr ; ::_thesis: for J being set for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds rng (netmap ((FinSups f),L)) c= finsups (rng f) let J be set ; ::_thesis: for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds rng (netmap ((FinSups f),L)) c= finsups (rng f) let f be Function of J, the carrier of L; ::_thesis: ( ( for x being set holds ex_sup_of f .: x,L ) implies rng (netmap ((FinSups f),L)) c= finsups (rng f) ) assume A1: for x being set holds ex_sup_of f .: x,L ; ::_thesis: rng (netmap ((FinSups f),L)) c= finsups (rng f) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng (netmap ((FinSups f),L)) or q in finsups (rng f) ) set h = netmap ((FinSups f),L); assume q in rng (netmap ((FinSups f),L)) ; ::_thesis: q in finsups (rng f) then consider x being set such that A2: x in dom (netmap ((FinSups f),L)) and A3: (netmap ((FinSups f),L)) . x = q by FUNCT_1:def_3; A4: ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2; then reconsider x = x as Element of Fin J by A2; A5: ( f .: x is finite Subset of (rng f) & ex_sup_of f .: x,L ) by A1, RELAT_1:111; (netmap ((FinSups f),L)) . x = sup (f .: x) by A4; hence q in finsups (rng f) by A3, A5; ::_thesis: verum end; theorem Th25: :: WAYBEL_2:25 for L being non empty reflexive antisymmetric RelStr for J being set for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L)) proof let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for J being set for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L)) let J be set ; ::_thesis: for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L)) let f be Function of J, the carrier of L; ::_thesis: rng f c= rng (netmap ((FinSups f),L)) percases ( not J is empty or J is empty ) ; supposeA1: not J is empty ; ::_thesis: rng f c= rng (netmap ((FinSups f),L)) let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng f or a in rng (netmap ((FinSups f),L)) ) assume a in rng f ; ::_thesis: a in rng (netmap ((FinSups f),L)) then consider b being set such that A2: b in dom f and A3: a = f . b by FUNCT_1:def_3; reconsider b = b as Element of J by A2; f . b in rng f by A2, FUNCT_1:def_3; then reconsider fb = f . b as Element of L ; A4: Im (f,b) = {fb} by A2, FUNCT_1:59; {b} c= J by A1, ZFMISC_1:31; then reconsider x = {b} as Element of Fin J by FINSUB_1:def_5; consider g being Function of (Fin J), the carrier of L such that A5: for x being Element of Fin J holds ( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2; dom g = Fin J by FUNCT_2:def_1; then A6: x in dom g ; g . {b} = sup (f .: x) by A5 .= a by A3, A4, YELLOW_0:39 ; hence a in rng (netmap ((FinSups f),L)) by A5, A6, FUNCT_1:def_3; ::_thesis: verum end; supposeA7: J is empty ; ::_thesis: rng f c= rng (netmap ((FinSups f),L)) rng f = {} by A7; hence rng f c= rng (netmap ((FinSups f),L)) by XBOOLE_1:2; ::_thesis: verum end; end; end; theorem Th26: :: WAYBEL_2:26 for L being non empty reflexive antisymmetric RelStr for J being set for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds Sup = sup (FinSups f) proof let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for J being set for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds Sup = sup (FinSups f) let J be set ; ::_thesis: for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds Sup = sup (FinSups f) let f be Function of J, the carrier of L; ::_thesis: ( ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) implies Sup = sup (FinSups f) ) assume that A1: ex_sup_of rng f,L and A2: ex_sup_of rng (netmap ((FinSups f),L)),L and A3: for x being Element of Fin J holds ex_sup_of f .: x,L ; ::_thesis: Sup = sup (FinSups f) set h = netmap ((FinSups f),L); A4: "\/" ((rng f),L) <= sup (rng (netmap ((FinSups f),L))) by A1, A2, Th25, YELLOW_0:34; rng (netmap ((FinSups f),L)) is_<=_than "\/" ((rng f),L) proof let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in rng (netmap ((FinSups f),L)) or a <= "\/" ((rng f),L) ) assume a in rng (netmap ((FinSups f),L)) ; ::_thesis: a <= "\/" ((rng f),L) then consider x being set such that A5: x in dom (netmap ((FinSups f),L)) and A6: a = (netmap ((FinSups f),L)) . x by FUNCT_1:def_3; A7: ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2; then reconsider x = x as Element of Fin J by A5; ex_sup_of f .: x,L by A3; then sup (f .: x) <= "\/" ((rng f),L) by A1, RELAT_1:111, YELLOW_0:34; hence a <= "\/" ((rng f),L) by A6, A7; ::_thesis: verum end; then A8: sup (rng (netmap ((FinSups f),L))) <= "\/" ((rng f),L) by A2, YELLOW_0:def_9; thus Sup = "\/" ((rng f),L) by YELLOW_2:def_5 .= sup (rng (netmap ((FinSups f),L))) by A4, A8, ORDERS_2:2 .= sup (FinSups f) by YELLOW_2:def_5 ; ::_thesis: verum end; theorem Th27: :: WAYBEL_2:27 for L being transitive antisymmetric with_infima RelStr for N being prenet of L for x being Element of L st N is eventually-directed holds x "/\" N is eventually-directed proof let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for N being prenet of L for x being Element of L st N is eventually-directed holds x "/\" N is eventually-directed let N be prenet of L; ::_thesis: for x being Element of L st N is eventually-directed holds x "/\" N is eventually-directed let x be Element of L; ::_thesis: ( N is eventually-directed implies x "/\" N is eventually-directed ) assume A1: N is eventually-directed ; ::_thesis: x "/\" N is eventually-directed A2: RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def3; for i being Element of (x "/\" N) ex j being Element of (x "/\" N) st for k being Element of (x "/\" N) st j <= k holds (x "/\" N) . i <= (x "/\" N) . k proof let i1 be Element of (x "/\" N); ::_thesis: ex j being Element of (x "/\" N) st for k being Element of (x "/\" N) st j <= k holds (x "/\" N) . i1 <= (x "/\" N) . k reconsider i = i1 as Element of N by Th22; consider j being Element of N such that A3: for k being Element of N st j <= k holds N . i <= N . k by A1, WAYBEL_0:11; reconsider j1 = j as Element of (x "/\" N) by Th22; take j1 ; ::_thesis: for k being Element of (x "/\" N) st j1 <= k holds (x "/\" N) . i1 <= (x "/\" N) . k let k1 be Element of (x "/\" N); ::_thesis: ( j1 <= k1 implies (x "/\" N) . i1 <= (x "/\" N) . k1 ) reconsider k = k1 as Element of N by Th22; assume j1 <= k1 ; ::_thesis: (x "/\" N) . i1 <= (x "/\" N) . k1 then j <= k by A2, YELLOW_0:1; then A4: N . i <= N . k by A3; ( ex yi being Element of L st ( yi = the mapping of N . i1 & the mapping of (x "/\" N) . i1 = x "/\" yi ) & ex yk being Element of L st ( yk = the mapping of N . k1 & the mapping of (x "/\" N) . k1 = x "/\" yk ) ) by Def3; hence (x "/\" N) . i1 <= (x "/\" N) . k1 by A4, WAYBEL_1:1; ::_thesis: verum end; hence x "/\" N is eventually-directed by WAYBEL_0:11; ::_thesis: verum end; theorem Th28: :: WAYBEL_2:28 for L being up-complete Semilattice st ( for x being Element of L for E being non empty directed Subset of L st x <= sup E holds x <= sup ({x} "/\" E) ) holds for D being non empty directed Subset of L for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D) proof let L be up-complete Semilattice; ::_thesis: ( ( for x being Element of L for E being non empty directed Subset of L st x <= sup E holds x <= sup ({x} "/\" E) ) implies for D being non empty directed Subset of L for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D) ) assume A1: for x being Element of L for E being non empty directed Subset of L st x <= sup E holds x <= sup ({x} "/\" E) ; ::_thesis: for D being non empty directed Subset of L for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D) let D be non empty directed Subset of L; ::_thesis: for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D) let x be Element of L; ::_thesis: x "/\" (sup D) = sup ({x} "/\" D) ex w being Element of L st ( x >= w & sup D >= w & ( for c being Element of L st x >= c & sup D >= c holds w >= c ) ) by LATTICE3:def_11; then x "/\" (sup D) <= sup D by LATTICE3:def_14; then A2: x "/\" (sup D) <= sup ({(x "/\" (sup D))} "/\" D) by A1; reconsider T = {(x "/\" (sup D))} as non empty directed Subset of L by WAYBEL_0:5; ex_sup_of D,L by WAYBEL_0:75; then A3: sup D is_>=_than D by YELLOW_0:30; ( ex_sup_of T "/\" D,L & {(x "/\" (sup D))} "/\" D is_<=_than x "/\" (sup D) ) by WAYBEL_0:75, YELLOW_4:52; then sup ({(x "/\" (sup D))} "/\" D) <= x "/\" (sup D) by YELLOW_0:30; hence x "/\" (sup D) = sup ({(x "/\" (sup D))} "/\" D) by A2, ORDERS_2:2 .= sup (({x} "/\" {(sup D)}) "/\" D) by YELLOW_4:46 .= sup ({x} "/\" ({(sup D)} "/\" D)) by YELLOW_4:41 .= sup ({x} "/\" D) by A3, YELLOW_4:51 ; ::_thesis: verum end; theorem :: WAYBEL_2:29 for L being with_suprema Poset st ( for X being directed Subset of L for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ) holds for X being Subset of L for x being Element of L st ex_sup_of X,L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) proof let L be with_suprema Poset; ::_thesis: ( ( for X being directed Subset of L for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ) implies for X being Subset of L for x being Element of L st ex_sup_of X,L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) ) assume A1: for X being directed Subset of L for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ; ::_thesis: for X being Subset of L for x being Element of L st ex_sup_of X,L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) let X be Subset of L; ::_thesis: for x being Element of L st ex_sup_of X,L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) let x be Element of L; ::_thesis: ( ex_sup_of X,L implies x "/\" (sup X) = sup ({x} "/\" (finsups X)) ) assume ex_sup_of X,L ; ::_thesis: x "/\" (sup X) = sup ({x} "/\" (finsups X)) hence x "/\" (sup X) = x "/\" (sup (finsups X)) by WAYBEL_0:55 .= sup ({x} "/\" (finsups X)) by A1 ; ::_thesis: verum end; theorem :: WAYBEL_2:30 for L being up-complete LATTICE st ( for X being Subset of L for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) ) holds for X being non empty directed Subset of L for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) proof let L be up-complete LATTICE; ::_thesis: ( ( for X being Subset of L for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) ) implies for X being non empty directed Subset of L for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ) assume A1: for X being Subset of L for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) ; ::_thesis: for X being non empty directed Subset of L for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) let X be non empty directed Subset of L; ::_thesis: for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) let x be Element of L; ::_thesis: x "/\" (sup X) = sup ({x} "/\" X) reconsider T = {x} as non empty directed Subset of L by WAYBEL_0:5; A2: ex_sup_of T "/\" X,L by WAYBEL_0:75; A3: {x} "/\" (finsups X) = { (x "/\" y) where y is Element of L : y in finsups X } by YELLOW_4:42; A4: {x} "/\" (finsups X) is_<=_than sup ({x} "/\" X) proof let q be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not q in {x} "/\" (finsups X) or q <= sup ({x} "/\" X) ) A5: x <= x ; assume q in {x} "/\" (finsups X) ; ::_thesis: q <= sup ({x} "/\" X) then consider y being Element of L such that A6: q = x "/\" y and A7: y in finsups X by A3; consider Y being finite Subset of X such that A8: y = "\/" (Y,L) and A9: ex_sup_of Y,L by A7; consider z being Element of L such that A10: z in X and A11: z is_>=_than Y by WAYBEL_0:1; "\/" (Y,L) <= z by A9, A11, YELLOW_0:30; then A12: x "/\" y <= x "/\" z by A8, A5, YELLOW_3:2; x in {x} by TARSKI:def_1; then x "/\" z <= sup ({x} "/\" X) by A2, A10, YELLOW_4:1, YELLOW_4:37; hence q <= sup ({x} "/\" X) by A6, A12, YELLOW_0:def_2; ::_thesis: verum end; ex_sup_of T "/\" (finsups X),L by WAYBEL_0:75; then sup ({x} "/\" (finsups X)) <= sup ({x} "/\" X) by A4, YELLOW_0:30; then A13: x "/\" (sup X) <= sup ({x} "/\" X) by A1; ex_sup_of X,L by WAYBEL_0:75; then sup ({x} "/\" X) <= x "/\" (sup X) by A2, YELLOW_4:53; hence x "/\" (sup X) = sup ({x} "/\" X) by A13, ORDERS_2:2; ::_thesis: verum end; begin definition let L be non empty RelStr ; func inf_op L -> Function of [:L,L:],L means :Def4: :: WAYBEL_2:def 4 for x, y being Element of L holds it . (x,y) = x "/\" y; existence ex b1 being Function of [:L,L:],L st for x, y being Element of L holds b1 . (x,y) = x "/\" y proof deffunc H1( Element of L, Element of L) -> Element of the carrier of L = $1 "/\" $2; A1: for x, y being Element of L holds H1(x,y) is Element of L ; consider f being Function of [:L,L:],L such that A2: for x, y being Element of L holds f . (x,y) = H1(x,y) from YELLOW_3:sch_6(A1); take f ; ::_thesis: for x, y being Element of L holds f . (x,y) = x "/\" y thus for x, y being Element of L holds f . (x,y) = x "/\" y by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . (x,y) = x "/\" y ) & ( for x, y being Element of L holds b2 . (x,y) = x "/\" y ) holds b1 = b2 proof let f, g be Function of [:L,L:],L; ::_thesis: ( ( for x, y being Element of L holds f . (x,y) = x "/\" y ) & ( for x, y being Element of L holds g . (x,y) = x "/\" y ) implies f = g ) assume that A3: for x, y being Element of L holds f . (x,y) = x "/\" y and A4: for x, y being Element of L holds g . (x,y) = x "/\" y ; ::_thesis: f = g now__::_thesis:_for_x,_y_being_Element_of_L_holds_f_._(x,y)_=_g_._(x,y) let x, y be Element of L; ::_thesis: f . (x,y) = g . (x,y) thus f . (x,y) = x "/\" y by A3 .= g . (x,y) by A4 ; ::_thesis: verum end; hence f = g by YELLOW_3:13; ::_thesis: verum end; end; :: deftheorem Def4 defines inf_op WAYBEL_2:def_4_:_ for L being non empty RelStr for b2 being Function of [:L,L:],L holds ( b2 = inf_op L iff for x, y being Element of L holds b2 . (x,y) = x "/\" y ); theorem Th31: :: WAYBEL_2:31 for L being non empty RelStr for x being Element of [:L,L:] holds (inf_op L) . x = (x `1) "/\" (x `2) proof let L be non empty RelStr ; ::_thesis: for x being Element of [:L,L:] holds (inf_op L) . x = (x `1) "/\" (x `2) let x be Element of [:L,L:]; ::_thesis: (inf_op L) . x = (x `1) "/\" (x `2) the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by YELLOW_3:def_2; then ex a, b being set st ( a in the carrier of L & b in the carrier of L & x = [a,b] ) by ZFMISC_1:def_2; hence (inf_op L) . x = (inf_op L) . ((x `1),(x `2)) by MCART_1:8 .= (x `1) "/\" (x `2) by Def4 ; ::_thesis: verum end; registration let L be transitive antisymmetric with_infima RelStr ; cluster inf_op L -> monotone ; coherence inf_op L is monotone proof let x, y be Element of [:L,L:]; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds ( not b1 = (inf_op L) . x or not b2 = (inf_op L) . y or b1 <= b2 ) ) set f = inf_op L; assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of L holds ( not b1 = (inf_op L) . x or not b2 = (inf_op L) . y or b1 <= b2 ) then A1: ( x `1 <= y `1 & x `2 <= y `2 ) by YELLOW_3:12; A2: ( (inf_op L) . x = (x `1) "/\" (x `2) & (inf_op L) . y = (y `1) "/\" (y `2) ) by Th31; let a, b be Element of L; ::_thesis: ( not a = (inf_op L) . x or not b = (inf_op L) . y or a <= b ) assume ( a = (inf_op L) . x & b = (inf_op L) . y ) ; ::_thesis: a <= b hence a <= b by A1, A2, YELLOW_3:2; ::_thesis: verum end; end; theorem Th32: :: WAYBEL_2:32 for S being non empty RelStr for D1, D2 being Subset of S holds (inf_op S) .: [:D1,D2:] = D1 "/\" D2 proof let S be non empty RelStr ; ::_thesis: for D1, D2 being Subset of S holds (inf_op S) .: [:D1,D2:] = D1 "/\" D2 let D1, D2 be Subset of S; ::_thesis: (inf_op S) .: [:D1,D2:] = D1 "/\" D2 set f = inf_op S; reconsider X = [:D1,D2:] as set ; thus (inf_op S) .: [:D1,D2:] c= D1 "/\" D2 :: according to XBOOLE_0:def_10 ::_thesis: D1 "/\" D2 c= (inf_op S) .: [:D1,D2:] proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (inf_op S) .: [:D1,D2:] or q in D1 "/\" D2 ) assume A1: q in (inf_op S) .: [:D1,D2:] ; ::_thesis: q in D1 "/\" D2 then reconsider q1 = q as Element of S ; consider c being Element of [:S,S:] such that A2: c in [:D1,D2:] and A3: q1 = (inf_op S) . c by A1, FUNCT_2:65; consider x, y being set such that A4: ( x in D1 & y in D2 ) and A5: c = [x,y] by A2, ZFMISC_1:def_2; reconsider x = x, y = y as Element of S by A4; q = (inf_op S) . (x,y) by A3, A5 .= x "/\" y by Def4 ; then q in { (a "/\" b) where a, b is Element of S : ( a in D1 & b in D2 ) } by A4; hence q in D1 "/\" D2 by YELLOW_4:def_4; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 "/\" D2 or q in (inf_op S) .: [:D1,D2:] ) assume q in D1 "/\" D2 ; ::_thesis: q in (inf_op S) .: [:D1,D2:] then q in { (x "/\" y) where x, y is Element of S : ( x in D1 & y in D2 ) } by YELLOW_4:def_4; then consider x, y being Element of S such that A6: ( q = x "/\" y & x in D1 & y in D2 ) ; ( q = (inf_op S) . (x,y) & [x,y] in X ) by A6, Def4, ZFMISC_1:87; hence q in (inf_op S) .: [:D1,D2:] by FUNCT_2:35; ::_thesis: verum end; theorem Th33: :: WAYBEL_2:33 for L being up-complete Semilattice for D being non empty directed Subset of [:L,L:] holds sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D)) proof let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D)) let D be non empty directed Subset of [:L,L:]; ::_thesis: sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D)) reconsider C = the carrier of L as non empty set ; reconsider D9 = D as non empty Subset of [:C,C:] by YELLOW_3:def_2; reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22; set f = inf_op L; A1: ex_sup_of D1 "/\" D2,L by WAYBEL_0:75; A2: (inf_op L) .: [:D1,D2:] = D1 "/\" D2 by Th32; A3: ( (inf_op L) .: [:D1,D2:] c= (inf_op L) .: (downarrow D) & (inf_op L) .: (downarrow D) c= downarrow ((inf_op L) .: D) ) by Th13, RELAT_1:123, YELLOW_3:48; A4: (inf_op L) .: D is directed by YELLOW_2:15; then A5: ex_sup_of (inf_op L) .: D,L by WAYBEL_0:75; ex_sup_of downarrow ((inf_op L) .: D),L by A4, WAYBEL_0:75; then sup (D1 "/\" D2) <= sup (downarrow ((inf_op L) .: D)) by A1, A3, A2, XBOOLE_1:1, YELLOW_0:34; then A6: sup (D1 "/\" D2) <= sup ((inf_op L) .: D) by A5, WAYBEL_0:33; (inf_op L) .: D9 c= (inf_op L) .: [:D1,D2:] by RELAT_1:123, YELLOW_3:1; then (inf_op L) .: D9 c= D1 "/\" D2 by Th32; then sup ((inf_op L) .: D) <= sup (D1 "/\" D2) by A5, A1, YELLOW_0:34; hence sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D)) by A6, ORDERS_2:2; ::_thesis: verum end; definition let L be non empty RelStr ; func sup_op L -> Function of [:L,L:],L means :Def5: :: WAYBEL_2:def 5 for x, y being Element of L holds it . (x,y) = x "\/" y; existence ex b1 being Function of [:L,L:],L st for x, y being Element of L holds b1 . (x,y) = x "\/" y proof deffunc H1( Element of L, Element of L) -> Element of the carrier of L = $1 "\/" $2; A1: for x, y being Element of L holds H1(x,y) is Element of L ; consider f being Function of [:L,L:],L such that A2: for x, y being Element of L holds f . (x,y) = H1(x,y) from YELLOW_3:sch_6(A1); take f ; ::_thesis: for x, y being Element of L holds f . (x,y) = x "\/" y thus for x, y being Element of L holds f . (x,y) = x "\/" y by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . (x,y) = x "\/" y ) & ( for x, y being Element of L holds b2 . (x,y) = x "\/" y ) holds b1 = b2 proof let f, g be Function of [:L,L:],L; ::_thesis: ( ( for x, y being Element of L holds f . (x,y) = x "\/" y ) & ( for x, y being Element of L holds g . (x,y) = x "\/" y ) implies f = g ) assume that A3: for x, y being Element of L holds f . (x,y) = x "\/" y and A4: for x, y being Element of L holds g . (x,y) = x "\/" y ; ::_thesis: f = g now__::_thesis:_for_x,_y_being_Element_of_L_holds_f_._(x,y)_=_g_._(x,y) let x, y be Element of L; ::_thesis: f . (x,y) = g . (x,y) thus f . (x,y) = x "\/" y by A3 .= g . (x,y) by A4 ; ::_thesis: verum end; hence f = g by YELLOW_3:13; ::_thesis: verum end; end; :: deftheorem Def5 defines sup_op WAYBEL_2:def_5_:_ for L being non empty RelStr for b2 being Function of [:L,L:],L holds ( b2 = sup_op L iff for x, y being Element of L holds b2 . (x,y) = x "\/" y ); theorem Th34: :: WAYBEL_2:34 for L being non empty RelStr for x being Element of [:L,L:] holds (sup_op L) . x = (x `1) "\/" (x `2) proof let L be non empty RelStr ; ::_thesis: for x being Element of [:L,L:] holds (sup_op L) . x = (x `1) "\/" (x `2) let x be Element of [:L,L:]; ::_thesis: (sup_op L) . x = (x `1) "\/" (x `2) the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by YELLOW_3:def_2; then ex a, b being set st ( a in the carrier of L & b in the carrier of L & x = [a,b] ) by ZFMISC_1:def_2; hence (sup_op L) . x = (sup_op L) . ((x `1),(x `2)) by MCART_1:8 .= (x `1) "\/" (x `2) by Def5 ; ::_thesis: verum end; registration let L be transitive antisymmetric with_suprema RelStr ; cluster sup_op L -> monotone ; coherence sup_op L is monotone proof let x, y be Element of [:L,L:]; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds ( not b1 = (sup_op L) . x or not b2 = (sup_op L) . y or b1 <= b2 ) ) set f = sup_op L; assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of L holds ( not b1 = (sup_op L) . x or not b2 = (sup_op L) . y or b1 <= b2 ) then A1: ( x `1 <= y `1 & x `2 <= y `2 ) by YELLOW_3:12; A2: ( (sup_op L) . x = (x `1) "\/" (x `2) & (sup_op L) . y = (y `1) "\/" (y `2) ) by Th34; let a, b be Element of L; ::_thesis: ( not a = (sup_op L) . x or not b = (sup_op L) . y or a <= b ) assume ( a = (sup_op L) . x & b = (sup_op L) . y ) ; ::_thesis: a <= b hence a <= b by A1, A2, YELLOW_3:3; ::_thesis: verum end; end; theorem Th35: :: WAYBEL_2:35 for S being non empty RelStr for D1, D2 being Subset of S holds (sup_op S) .: [:D1,D2:] = D1 "\/" D2 proof let S be non empty RelStr ; ::_thesis: for D1, D2 being Subset of S holds (sup_op S) .: [:D1,D2:] = D1 "\/" D2 let D1, D2 be Subset of S; ::_thesis: (sup_op S) .: [:D1,D2:] = D1 "\/" D2 set f = sup_op S; reconsider X = [:D1,D2:] as set ; thus (sup_op S) .: [:D1,D2:] c= D1 "\/" D2 :: according to XBOOLE_0:def_10 ::_thesis: D1 "\/" D2 c= (sup_op S) .: [:D1,D2:] proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (sup_op S) .: [:D1,D2:] or q in D1 "\/" D2 ) assume A1: q in (sup_op S) .: [:D1,D2:] ; ::_thesis: q in D1 "\/" D2 then reconsider q1 = q as Element of S ; consider c being Element of [:S,S:] such that A2: c in [:D1,D2:] and A3: q1 = (sup_op S) . c by A1, FUNCT_2:65; consider x, y being set such that A4: ( x in D1 & y in D2 ) and A5: c = [x,y] by A2, ZFMISC_1:def_2; reconsider x = x, y = y as Element of S by A4; q = (sup_op S) . (x,y) by A3, A5 .= x "\/" y by Def5 ; then q in { (a "\/" b) where a, b is Element of S : ( a in D1 & b in D2 ) } by A4; hence q in D1 "\/" D2 by YELLOW_4:def_3; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 "\/" D2 or q in (sup_op S) .: [:D1,D2:] ) assume q in D1 "\/" D2 ; ::_thesis: q in (sup_op S) .: [:D1,D2:] then q in { (x "\/" y) where x, y is Element of S : ( x in D1 & y in D2 ) } by YELLOW_4:def_3; then consider x, y being Element of S such that A6: ( q = x "\/" y & x in D1 & y in D2 ) ; ( q = (sup_op S) . (x,y) & [x,y] in X ) by A6, Def5, ZFMISC_1:87; hence q in (sup_op S) .: [:D1,D2:] by FUNCT_2:35; ::_thesis: verum end; theorem :: WAYBEL_2:36 for L being non empty complete Poset for D being non empty filtered Subset of [:L,L:] holds inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D)) proof let L be non empty complete Poset; ::_thesis: for D being non empty filtered Subset of [:L,L:] holds inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D)) let D be non empty filtered Subset of [:L,L:]; ::_thesis: inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D)) reconsider C = the carrier of L as non empty set ; reconsider D9 = D as non empty Subset of [:C,C:] by YELLOW_3:def_2; set D1 = proj1 D; set D2 = proj2 D; set f = sup_op L; A1: ex_inf_of (proj1 D) "\/" (proj2 D),L by YELLOW_0:17; A2: ( ex_inf_of uparrow ((sup_op L) .: D),L & (sup_op L) .: [:(proj1 D),(proj2 D):] c= (sup_op L) .: (uparrow D) ) by RELAT_1:123, YELLOW_0:17, YELLOW_3:49; ( (sup_op L) .: (uparrow D) c= uparrow ((sup_op L) .: D) & (sup_op L) .: [:(proj1 D),(proj2 D):] = (proj1 D) "\/" (proj2 D) ) by Th14, Th35; then inf ((proj1 D) "\/" (proj2 D)) >= inf (uparrow ((sup_op L) .: D)) by A1, A2, XBOOLE_1:1, YELLOW_0:35; then A3: inf ((proj1 D) "\/" (proj2 D)) >= inf ((sup_op L) .: D) by WAYBEL_0:38, YELLOW_0:17; (sup_op L) .: D9 c= (sup_op L) .: [:(proj1 D),(proj2 D):] by RELAT_1:123, YELLOW_3:1; then ( ex_inf_of (sup_op L) .: D9,L & (sup_op L) .: D9 c= (proj1 D) "\/" (proj2 D) ) by Th35, YELLOW_0:17; then inf ((sup_op L) .: D) >= inf ((proj1 D) "\/" (proj2 D)) by A1, YELLOW_0:35; hence inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D)) by A3, ORDERS_2:2; ::_thesis: verum end; begin definition let R be non empty reflexive RelStr ; attrR is satisfying_MC means :Def6: :: WAYBEL_2:def 6 for x being Element of R for D being non empty directed Subset of R holds x "/\" (sup D) = sup ({x} "/\" D); end; :: deftheorem Def6 defines satisfying_MC WAYBEL_2:def_6_:_ for R being non empty reflexive RelStr holds ( R is satisfying_MC iff for x being Element of R for D being non empty directed Subset of R holds x "/\" (sup D) = sup ({x} "/\" D) ); definition let R be non empty reflexive RelStr ; attrR is meet-continuous means :Def7: :: WAYBEL_2:def 7 ( R is up-complete & R is satisfying_MC ); end; :: deftheorem Def7 defines meet-continuous WAYBEL_2:def_7_:_ for R being non empty reflexive RelStr holds ( R is meet-continuous iff ( R is up-complete & R is satisfying_MC ) ); registration cluster1 -element reflexive -> 1 -element reflexive satisfying_MC for RelStr ; coherence for b1 being 1 -element reflexive RelStr holds b1 is satisfying_MC proof let I be 1 -element reflexive RelStr ; ::_thesis: I is satisfying_MC let x be Element of I; :: according to WAYBEL_2:def_6 ::_thesis: for D being non empty directed Subset of I holds x "/\" (sup D) = sup ({x} "/\" D) let D be non empty directed Subset of I; ::_thesis: x "/\" (sup D) = sup ({x} "/\" D) thus x "/\" (sup D) = sup ({x} "/\" D) by STRUCT_0:def_10; ::_thesis: verum end; end; registration cluster non empty reflexive meet-continuous -> non empty reflexive up-complete satisfying_MC for RelStr ; coherence for b1 being non empty reflexive RelStr st b1 is meet-continuous holds ( b1 is up-complete & b1 is satisfying_MC ) by Def7; cluster non empty reflexive up-complete satisfying_MC -> non empty reflexive meet-continuous for RelStr ; coherence for b1 being non empty reflexive RelStr st b1 is up-complete & b1 is satisfying_MC holds b1 is meet-continuous by Def7; end; theorem Th37: :: WAYBEL_2:37 for S being non empty reflexive RelStr st ( for X being Subset of S for x being Element of S holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) holds S is satisfying_MC proof let S be non empty reflexive RelStr ; ::_thesis: ( ( for X being Subset of S for x being Element of S holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) implies S is satisfying_MC ) assume A1: for X being Subset of S for x being Element of S holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ; ::_thesis: S is satisfying_MC let y be Element of S; :: according to WAYBEL_2:def_6 ::_thesis: for D being non empty directed Subset of S holds y "/\" (sup D) = sup ({y} "/\" D) let D be non empty directed Subset of S; ::_thesis: y "/\" (sup D) = sup ({y} "/\" D) thus sup ({y} "/\" D) = "\/" ( { (y "/\" z) where z is Element of S : z in D } ,S) by YELLOW_4:42 .= y "/\" (sup D) by A1 ; ::_thesis: verum end; theorem Th38: :: WAYBEL_2:38 for L being up-complete Semilattice st SupMap L is meet-preserving holds for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) proof let L be up-complete Semilattice; ::_thesis: ( SupMap L is meet-preserving implies for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) assume A1: SupMap L is meet-preserving ; ::_thesis: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) set f = SupMap L; let I1, I2 be Ideal of L; ::_thesis: (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) reconsider x = I1, y = I2 as Element of (InclPoset (Ids L)) by YELLOW_2:41; A2: SupMap L preserves_inf_of {x,y} by A1, WAYBEL_0:def_34; reconsider fx = (SupMap L) . x as Element of L ; thus (sup I1) "/\" (sup I2) = fx "/\" (sup I2) by YELLOW_2:def_3 .= ((SupMap L) . x) "/\" ((SupMap L) . y) by YELLOW_2:def_3 .= (SupMap L) . (x "/\" y) by A2, YELLOW_3:8 .= (SupMap L) . (I1 "/\" I2) by YELLOW_4:58 .= sup (I1 "/\" I2) by YELLOW_2:def_3 ; ::_thesis: verum end; registration let L be up-complete sup-Semilattice; cluster SupMap L -> join-preserving ; coherence SupMap L is join-preserving proof let x, y be Element of (InclPoset (Ids L)); :: according to WAYBEL_0:def_35 ::_thesis: SupMap L preserves_sup_of {x,y} set f = SupMap L; assume ex_sup_of {x,y}, InclPoset (Ids L) ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (SupMap L) .: {x,y},L & "\/" (((SupMap L) .: {x,y}),L) = (SupMap L) . ("\/" ({x,y},(InclPoset (Ids L)))) ) reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2:41; A1: ex_sup_of x1 "\/" y1,L by WAYBEL_0:75; A2: dom (SupMap L) = the carrier of (InclPoset (Ids L)) by FUNCT_2:def_1; then (SupMap L) .: {x,y} = {((SupMap L) . x),((SupMap L) . y)} by FUNCT_1:60; hence ex_sup_of (SupMap L) .: {x,y},L by YELLOW_0:20; ::_thesis: "\/" (((SupMap L) .: {x,y}),L) = (SupMap L) . ("\/" ({x,y},(InclPoset (Ids L)))) thus sup ((SupMap L) .: {x,y}) = sup {((SupMap L) . x),((SupMap L) . y)} by A2, FUNCT_1:60 .= ((SupMap L) . x) "\/" ((SupMap L) . y) by YELLOW_0:41 .= ((SupMap L) . x) "\/" (sup y1) by YELLOW_2:def_3 .= (sup x1) "\/" (sup y1) by YELLOW_2:def_3 .= sup (x1 "\/" y1) by Th4 .= sup (downarrow (x1 "\/" y1)) by A1, WAYBEL_0:33 .= (SupMap L) . (downarrow (x1 "\/" y1)) by YELLOW_2:def_3 .= (SupMap L) . (x "\/" y) by YELLOW_4:30 .= (SupMap L) . (sup {x,y}) by YELLOW_0:41 ; ::_thesis: verum end; end; theorem Th39: :: WAYBEL_2:39 for L being up-complete Semilattice st ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) holds SupMap L is meet-preserving proof let L be up-complete Semilattice; ::_thesis: ( ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) implies SupMap L is meet-preserving ) assume A1: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ; ::_thesis: SupMap L is meet-preserving let x, y be Element of (InclPoset (Ids L)); :: according to WAYBEL_0:def_34 ::_thesis: SupMap L preserves_inf_of {x,y} set f = SupMap L; assume ex_inf_of {x,y}, InclPoset (Ids L) ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (SupMap L) .: {x,y},L & "/\" (((SupMap L) .: {x,y}),L) = (SupMap L) . ("/\" ({x,y},(InclPoset (Ids L)))) ) reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2:41; A2: dom (SupMap L) = the carrier of (InclPoset (Ids L)) by FUNCT_2:def_1; then (SupMap L) .: {x,y} = {((SupMap L) . x),((SupMap L) . y)} by FUNCT_1:60; hence ex_inf_of (SupMap L) .: {x,y},L by YELLOW_0:21; ::_thesis: "/\" (((SupMap L) .: {x,y}),L) = (SupMap L) . ("/\" ({x,y},(InclPoset (Ids L)))) thus inf ((SupMap L) .: {x,y}) = inf {((SupMap L) . x),((SupMap L) . y)} by A2, FUNCT_1:60 .= ((SupMap L) . x) "/\" ((SupMap L) . y) by YELLOW_0:40 .= ((SupMap L) . x) "/\" (sup y1) by YELLOW_2:def_3 .= (sup x1) "/\" (sup y1) by YELLOW_2:def_3 .= sup (x1 "/\" y1) by A1 .= (SupMap L) . (x1 "/\" y1) by YELLOW_2:def_3 .= (SupMap L) . (x "/\" y) by YELLOW_4:58 .= (SupMap L) . (inf {x,y}) by YELLOW_0:40 ; ::_thesis: verum end; theorem Th40: :: WAYBEL_2:40 for L being up-complete Semilattice st ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) holds for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) proof let L be up-complete Semilattice; ::_thesis: ( ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) implies for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) assume A1: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ; ::_thesis: for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) let D1, D2 be non empty directed Subset of L; ::_thesis: (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) A2: ex_sup_of D2,L by WAYBEL_0:75; A3: ex_sup_of (downarrow D1) "/\" (downarrow D2),L by WAYBEL_0:75; A4: ex_sup_of D1 "/\" D2,L by WAYBEL_0:75; ex_sup_of D1,L by WAYBEL_0:75; hence (sup D1) "/\" (sup D2) = (sup (downarrow D1)) "/\" (sup D2) by WAYBEL_0:33 .= (sup (downarrow D1)) "/\" (sup (downarrow D2)) by A2, WAYBEL_0:33 .= sup ((downarrow D1) "/\" (downarrow D2)) by A1 .= sup (downarrow ((downarrow D1) "/\" (downarrow D2))) by A3, WAYBEL_0:33 .= sup (downarrow (D1 "/\" D2)) by YELLOW_4:62 .= sup (D1 "/\" D2) by A4, WAYBEL_0:33 ; ::_thesis: verum end; theorem Th41: :: WAYBEL_2:41 for L being non empty reflexive RelStr st L is satisfying_MC holds for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) proof let L be non empty reflexive RelStr ; ::_thesis: ( L is satisfying_MC implies for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) assume A1: L is satisfying_MC ; ::_thesis: for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) let x be Element of L; ::_thesis: for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) let N be prenet of L; ::_thesis: ( N is eventually-directed implies x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) assume N is eventually-directed ; ::_thesis: x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) then A2: rng (netmap (N,L)) is directed by Th18; thus x "/\" (sup N) = x "/\" (sup (rng (netmap (N,L)))) by YELLOW_2:def_5 .= sup ({x} "/\" (rng (netmap (N,L)))) by A1, A2, Def6 ; ::_thesis: verum end; theorem Th42: :: WAYBEL_2:42 for L being non empty reflexive RelStr st ( for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds L is satisfying_MC proof let L be non empty reflexive RelStr ; ::_thesis: ( ( for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) implies L is satisfying_MC ) assume A1: for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ; ::_thesis: L is satisfying_MC let x be Element of L; :: according to WAYBEL_2:def_6 ::_thesis: for D being non empty directed Subset of L holds x "/\" (sup D) = sup ({x} "/\" D) let D be non empty directed Subset of L; ::_thesis: x "/\" (sup D) = sup ({x} "/\" D) reconsider n = id D as Function of D, the carrier of L by FUNCT_2:7; reconsider N = NetStr(# D,( the InternalRel of L |_2 D),n #) as prenet of L by Th19; A2: Sup = sup N ; D c= D ; then A3: D = n .: D by FUNCT_1:92 .= rng (netmap (N,L)) by RELSET_1:22 ; hence x "/\" (sup D) = x "/\" (Sup ) by YELLOW_2:def_5 .= sup ({x} "/\" D) by A1, A3, A2, Th20 ; ::_thesis: verum end; theorem Th43: :: WAYBEL_2:43 for L being non empty reflexive antisymmetric up-complete RelStr st inf_op L is directed-sups-preserving holds for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) proof let L be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: ( inf_op L is directed-sups-preserving implies for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) assume A1: inf_op L is directed-sups-preserving ; ::_thesis: for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) let D1, D2 be non empty directed Subset of L; ::_thesis: (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) set X = [:D1,D2:]; set f = inf_op L; A2: inf_op L preserves_sup_of [:D1,D2:] by A1, WAYBEL_0:def_37; A3: ex_sup_of [:D1,D2:],[:L,L:] by WAYBEL_0:75; A4: ( ex_sup_of D1,L & ex_sup_of D2,L ) by WAYBEL_0:75; thus (sup D1) "/\" (sup D2) = (inf_op L) . ((sup D1),(sup D2)) by Def4 .= (inf_op L) . (sup [:D1,D2:]) by A4, YELLOW_3:43 .= sup ((inf_op L) .: [:D1,D2:]) by A2, A3, WAYBEL_0:def_31 .= sup (D1 "/\" D2) by Th32 ; ::_thesis: verum end; theorem Th44: :: WAYBEL_2:44 for L being non empty reflexive antisymmetric RelStr st ( for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) holds L is satisfying_MC proof let L be non empty reflexive antisymmetric RelStr ; ::_thesis: ( ( for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) implies L is satisfying_MC ) assume A1: for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ; ::_thesis: L is satisfying_MC let x be Element of L; :: according to WAYBEL_2:def_6 ::_thesis: for D being non empty directed Subset of L holds x "/\" (sup D) = sup ({x} "/\" D) let D be non empty directed Subset of L; ::_thesis: x "/\" (sup D) = sup ({x} "/\" D) A2: {x} is directed by WAYBEL_0:5; thus x "/\" (sup D) = (sup {x}) "/\" (sup D) by YELLOW_0:39 .= sup ({x} "/\" D) by A1, A2 ; ::_thesis: verum end; theorem Th45: :: WAYBEL_2:45 for L being non empty reflexive antisymmetric with_infima satisfying_MC RelStr for x being Element of L for D being non empty directed Subset of L st x <= sup D holds x = sup ({x} "/\" D) proof let L be non empty reflexive antisymmetric with_infima satisfying_MC RelStr ; ::_thesis: for x being Element of L for D being non empty directed Subset of L st x <= sup D holds x = sup ({x} "/\" D) let x be Element of L; ::_thesis: for D being non empty directed Subset of L st x <= sup D holds x = sup ({x} "/\" D) let D be non empty directed Subset of L; ::_thesis: ( x <= sup D implies x = sup ({x} "/\" D) ) assume x <= sup D ; ::_thesis: x = sup ({x} "/\" D) hence x = x "/\" (sup D) by YELLOW_0:25 .= sup ({x} "/\" D) by Def6 ; ::_thesis: verum end; theorem Th46: :: WAYBEL_2:46 for L being up-complete Semilattice st ( for x being Element of L for E being non empty directed Subset of L st x <= sup E holds x <= sup ({x} "/\" E) ) holds inf_op L is directed-sups-preserving proof let L be up-complete Semilattice; ::_thesis: ( ( for x being Element of L for E being non empty directed Subset of L st x <= sup E holds x <= sup ({x} "/\" E) ) implies inf_op L is directed-sups-preserving ) assume A1: for x being Element of L for E being non empty directed Subset of L st x <= sup E holds x <= sup ({x} "/\" E) ; ::_thesis: inf_op L is directed-sups-preserving let D be Subset of [:L,L:]; :: according to WAYBEL_0:def_37 ::_thesis: ( D is empty or not D is directed or inf_op L preserves_sup_of D ) assume ( not D is empty & D is directed ) ; ::_thesis: inf_op L preserves_sup_of D then reconsider DD = D as non empty directed Subset of [:L,L:] ; thus inf_op L preserves_sup_of D ::_thesis: verum proof reconsider D1 = proj1 DD, D2 = proj2 DD as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22; reconsider C = the carrier of L as non empty set ; set f = inf_op L; assume ex_sup_of D,[:L,L:] ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (inf_op L) .: D,L & "\/" (((inf_op L) .: D),L) = (inf_op L) . ("\/" (D,[:L,L:])) ) set d2 = sup D2; defpred S1[ set ] means ex x being Element of L st ( $1 = {x} "/\" D2 & x in D1 ); (inf_op L) .: DD is directed by YELLOW_2:15; hence ex_sup_of (inf_op L) .: D,L by WAYBEL_0:75; ::_thesis: "\/" (((inf_op L) .: D),L) = (inf_op L) . ("\/" (D,[:L,L:])) { (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } c= C proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } or q in C ) assume q in { (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } ; ::_thesis: q in C then ex x, y being Element of L st ( q = x "/\" y & x in D1 & y in {(sup D2)} ) ; hence q in C ; ::_thesis: verum end; then reconsider F = { (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } as Subset of L ; A2: "\/" ( { (sup X) where X is non empty directed Subset of L : S1[X] } ,L) = "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) by Th10; A3: F = { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } proof thus F c= { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } :: according to XBOOLE_0:def_10 ::_thesis: { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } c= F proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F or q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } ) assume q in F ; ::_thesis: q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } then consider x, y being Element of L such that A4: q = x "/\" y and A5: x in D1 and A6: y in {(sup D2)} ; q = x "/\" (sup D2) by A4, A6, TARSKI:def_1 .= sup ({x} "/\" D2) by A1, Th28 ; hence q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } by A5; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } or q in F ) A7: sup D2 in {(sup D2)} by TARSKI:def_1; assume q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } ; ::_thesis: q in F then consider z being Element of L such that A8: q = sup ({z} "/\" D2) and A9: z in D1 ; q = z "/\" (sup D2) by A1, A8, Th28; hence q in F by A9, A7; ::_thesis: verum end; thus sup ((inf_op L) .: D) = sup (D1 "/\" D2) by Th33 .= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) by A2, Th6 .= "\/" ( { (sup ({x} "/\" D2)) where x is Element of L : x in D1 } ,L) by Th5 .= sup ({(sup D2)} "/\" D1) by A3, YELLOW_4:def_4 .= (sup D1) "/\" (sup D2) by A1, Th28 .= (inf_op L) . ((sup D1),(sup D2)) by Def4 .= (inf_op L) . (sup D) by Th12 ; ::_thesis: verum end; end; theorem Th47: :: WAYBEL_2:47 for L being non empty reflexive antisymmetric complete RelStr st ( for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds for x being Element of L for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) proof let L be non empty reflexive antisymmetric complete RelStr ; ::_thesis: ( ( for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) implies for x being Element of L for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) assume A1: for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ; ::_thesis: for x being Element of L for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) let x be Element of L; ::_thesis: for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) let J be set ; ::_thesis: for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) let f be Function of J, the carrier of L; ::_thesis: x "/\" (Sup ) = sup (x "/\" (FinSups f)) set F = FinSups f; A2: for x being Element of Fin J holds ex_sup_of f .: x,L by YELLOW_0:17; ( ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L ) by YELLOW_0:17; hence x "/\" (Sup ) = x "/\" (sup (FinSups f)) by A2, Th26 .= sup ({x} "/\" (rng (netmap ((FinSups f),L)))) by A1 .= "\/" ((rng the mapping of (x "/\" (FinSups f))),L) by Th23 .= sup (x "/\" (FinSups f)) by YELLOW_2:def_5 ; ::_thesis: verum end; theorem Th48: :: WAYBEL_2:48 for L being complete Semilattice st ( for x being Element of L for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) holds for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) proof let L be complete Semilattice; ::_thesis: ( ( for x being Element of L for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) implies for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) assume A1: for x being Element of L for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ; ::_thesis: for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) let x be Element of L; ::_thesis: for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) let N be prenet of L; ::_thesis: ( N is eventually-directed implies x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) assume A2: N is eventually-directed ; ::_thesis: x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) reconsider R = rng (netmap (N,L)) as non empty directed Subset of L by A2, Th18; reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5; set f = the mapping of N; set h = the mapping of (FinSups the mapping of N); A3: ex_sup_of xx "/\" R,L by WAYBEL_0:75; A4: rng the mapping of (x "/\" (FinSups the mapping of N)) is_<=_than sup ({x} "/\" (rng (netmap (N,L)))) proof let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in rng the mapping of (x "/\" (FinSups the mapping of N)) or a <= sup ({x} "/\" (rng (netmap (N,L)))) ) A5: {x} "/\" (rng the mapping of (FinSups the mapping of N)) = { (x "/\" y) where y is Element of L : y in rng the mapping of (FinSups the mapping of N) } by YELLOW_4:42; assume a in rng the mapping of (x "/\" (FinSups the mapping of N)) ; ::_thesis: a <= sup ({x} "/\" (rng (netmap (N,L)))) then a in {x} "/\" (rng the mapping of (FinSups the mapping of N)) by Th23; then consider y being Element of L such that A6: a = x "/\" y and A7: y in rng the mapping of (FinSups the mapping of N) by A5; for x being set holds ex_sup_of the mapping of N .: x,L by YELLOW_0:17; then rng (netmap ((FinSups the mapping of N),L)) c= finsups (rng the mapping of N) by Th24; then y in finsups (rng the mapping of N) by A7; then consider Y being finite Subset of (rng the mapping of N) such that A8: y = "\/" (Y,L) and A9: ex_sup_of Y,L ; rng (netmap (N,L)) is directed by A2, Th18; then consider z being Element of L such that A10: z in rng the mapping of N and A11: z is_>=_than Y by WAYBEL_0:1; A12: x <= x ; "\/" (Y,L) <= z by A9, A11, YELLOW_0:30; then A13: x "/\" y <= x "/\" z by A8, A12, YELLOW_3:2; x in {x} by TARSKI:def_1; then x "/\" z <= sup (xx "/\" (rng the mapping of N)) by A3, A10, YELLOW_4:1, YELLOW_4:37; hence a <= sup ({x} "/\" (rng (netmap (N,L)))) by A6, A13, YELLOW_0:def_2; ::_thesis: verum end; x "/\" (FinSups the mapping of N) is eventually-directed by Th27; then rng (netmap ((x "/\" (FinSups the mapping of N)),L)) is directed by Th18; then ex_sup_of rng the mapping of (x "/\" (FinSups the mapping of N)),L by WAYBEL_0:75; then ( sup (x "/\" (FinSups the mapping of N)) = "\/" ((rng the mapping of (x "/\" (FinSups the mapping of N))),L) & "\/" ((rng the mapping of (x "/\" (FinSups the mapping of N))),L) <= sup ({x} "/\" (rng (netmap (N,L)))) ) by A4, YELLOW_0:def_9, YELLOW_2:def_5; then A14: x "/\" (Sup ) <= sup ({x} "/\" (rng (netmap (N,L)))) by A1; ( ex_sup_of R,L & Sup = "\/" ((rng (netmap (N,L))),L) ) by WAYBEL_0:75, YELLOW_2:def_5; then sup ({x} "/\" (rng (netmap (N,L)))) <= x "/\" (Sup ) by A3, YELLOW_4:53; hence x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) by A14, ORDERS_2:2; ::_thesis: verum end; theorem Th49: :: WAYBEL_2:49 for L being up-complete LATTICE holds ( L is meet-continuous iff ( SupMap L is meet-preserving & SupMap L is join-preserving ) ) proof let L be up-complete LATTICE; ::_thesis: ( L is meet-continuous iff ( SupMap L is meet-preserving & SupMap L is join-preserving ) ) hereby ::_thesis: ( SupMap L is meet-preserving & SupMap L is join-preserving implies L is meet-continuous ) assume A1: L is meet-continuous ; ::_thesis: ( SupMap L is meet-preserving & SupMap L is join-preserving ) for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) proof let D1, D2 be non empty directed Subset of L; ::_thesis: (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) for x being Element of L for E being non empty directed Subset of L st x <= sup E holds x <= sup ({x} "/\" E) by A1, Th45; then inf_op L is directed-sups-preserving by Th46; hence (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43; ::_thesis: verum end; then for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ; hence ( SupMap L is meet-preserving & SupMap L is join-preserving ) by Th39; ::_thesis: verum end; assume A2: ( SupMap L is meet-preserving & SupMap L is join-preserving ) ; ::_thesis: L is meet-continuous thus L is up-complete ; :: according to WAYBEL_2:def_7 ::_thesis: L is satisfying_MC for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) by A2, Th38; then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th40; hence L is satisfying_MC by Th44; ::_thesis: verum end; registration let L be meet-continuous LATTICE; cluster SupMap L -> meet-preserving join-preserving ; coherence ( SupMap L is meet-preserving & SupMap L is join-preserving ) by Th49; end; theorem Th50: :: WAYBEL_2:50 for L being up-complete LATTICE holds ( L is meet-continuous iff for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) proof let L be up-complete LATTICE; ::_thesis: ( L is meet-continuous iff for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) hereby ::_thesis: ( ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) implies L is meet-continuous ) assume L is meet-continuous ; ::_thesis: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) then ( SupMap L is meet-preserving & SupMap L is join-preserving ) ; hence for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) by Th38; ::_thesis: verum end; assume for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ; ::_thesis: L is meet-continuous then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th40; hence ( L is up-complete & L is satisfying_MC ) by Th44; :: according to WAYBEL_2:def_7 ::_thesis: verum end; theorem Th51: :: WAYBEL_2:51 for L being up-complete LATTICE holds ( L is meet-continuous iff for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) proof let L be up-complete LATTICE; ::_thesis: ( L is meet-continuous iff for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) hereby ::_thesis: ( ( for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) implies L is meet-continuous ) assume L is meet-continuous ; ::_thesis: for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) then for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) by Th50; hence for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th40; ::_thesis: verum end; assume for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ; ::_thesis: L is meet-continuous hence ( L is up-complete & L is satisfying_MC ) by Th44; :: according to WAYBEL_2:def_7 ::_thesis: verum end; theorem :: WAYBEL_2:52 for L being up-complete LATTICE holds ( L is meet-continuous iff for x being Element of L for D being non empty directed Subset of L st x <= sup D holds x = sup ({x} "/\" D) ) proof let L be up-complete LATTICE; ::_thesis: ( L is meet-continuous iff for x being Element of L for D being non empty directed Subset of L st x <= sup D holds x = sup ({x} "/\" D) ) thus ( L is meet-continuous implies for x being Element of L for D being non empty directed Subset of L st x <= sup D holds x = sup ({x} "/\" D) ) by Th45; ::_thesis: ( ( for x being Element of L for D being non empty directed Subset of L st x <= sup D holds x = sup ({x} "/\" D) ) implies L is meet-continuous ) assume for x being Element of L for D being non empty directed Subset of L st x <= sup D holds x = sup ({x} "/\" D) ; ::_thesis: L is meet-continuous then for x being Element of L for D being non empty directed Subset of L st x <= sup D holds x <= sup ({x} "/\" D) ; then inf_op L is directed-sups-preserving by Th46; then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43; hence L is meet-continuous by Th51; ::_thesis: verum end; theorem Th53: :: WAYBEL_2:53 for L being up-complete Semilattice holds ( L is meet-continuous iff inf_op L is directed-sups-preserving ) proof let L be up-complete Semilattice; ::_thesis: ( L is meet-continuous iff inf_op L is directed-sups-preserving ) hereby ::_thesis: ( inf_op L is directed-sups-preserving implies L is meet-continuous ) assume L is meet-continuous ; ::_thesis: inf_op L is directed-sups-preserving then for x being Element of L for D being non empty directed Subset of L st x <= sup D holds x <= sup ({x} "/\" D) by Th45; hence inf_op L is directed-sups-preserving by Th46; ::_thesis: verum end; assume inf_op L is directed-sups-preserving ; ::_thesis: L is meet-continuous then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43; hence ( L is up-complete & L is satisfying_MC ) by Th44; :: according to WAYBEL_2:def_7 ::_thesis: verum end; registration let L be meet-continuous Semilattice; cluster inf_op L -> directed-sups-preserving ; coherence inf_op L is directed-sups-preserving by Th53; end; theorem Th54: :: WAYBEL_2:54 for L being up-complete Semilattice holds ( L is meet-continuous iff for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) proof let L be up-complete Semilattice; ::_thesis: ( L is meet-continuous iff for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) thus ( L is meet-continuous implies for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) by Th41; ::_thesis: ( ( for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) implies L is meet-continuous ) assume for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ; ::_thesis: L is meet-continuous hence ( L is up-complete & L is satisfying_MC ) by Th42; :: according to WAYBEL_2:def_7 ::_thesis: verum end; theorem :: WAYBEL_2:55 for L being complete Semilattice holds ( L is meet-continuous iff for x being Element of L for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) proof let L be complete Semilattice; ::_thesis: ( L is meet-continuous iff for x being Element of L for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) hereby ::_thesis: ( ( for x being Element of L for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) implies L is meet-continuous ) assume L is meet-continuous ; ::_thesis: for x being Element of L for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) then for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) by Th54; hence for x being Element of L for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) by Th47; ::_thesis: verum end; assume for x being Element of L for J being set for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ; ::_thesis: L is meet-continuous then for x being Element of L for N being prenet of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) by Th48; hence ( L is up-complete & L is satisfying_MC ) by Th42; :: according to WAYBEL_2:def_7 ::_thesis: verum end; Lm1: for L being meet-continuous Semilattice for x being Element of L holds x "/\" is directed-sups-preserving proof let L be meet-continuous Semilattice; ::_thesis: for x being Element of L holds x "/\" is directed-sups-preserving let x be Element of L; ::_thesis: x "/\" 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 x "/\" preserves_sup_of X ) assume A1: ( not X is empty & X is directed ) ; ::_thesis: x "/\" preserves_sup_of X reconsider X1 = X as non empty Subset of L by A1; assume ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (x "/\") .: X,L & "\/" (((x "/\") .: X),L) = (x "/\") . ("\/" (X,L)) ) A2: not (x "/\") .: X1 is empty ; (x "/\") .: X is directed by A1, YELLOW_2:15; hence ex_sup_of (x "/\") .: X,L by A2, WAYBEL_0:75; ::_thesis: "\/" (((x "/\") .: X),L) = (x "/\") . ("\/" (X,L)) A3: for x being Element of L for E being non empty directed Subset of L st x <= sup E holds x <= sup ({x} "/\" E) by Th45; thus sup ((x "/\") .: X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by WAYBEL_1:61 .= sup ({x} "/\" X) by YELLOW_4:42 .= x "/\" (sup X) by A1, A3, Th28 .= (x "/\") . (sup X) by WAYBEL_1:def_18 ; ::_thesis: verum end; registration let L be meet-continuous Semilattice; let x be Element of L; clusterx "/\" -> directed-sups-preserving ; coherence x "/\" is directed-sups-preserving by Lm1; end; theorem Th56: :: WAYBEL_2:56 for H being non empty complete Poset holds ( H is Heyting iff ( H is meet-continuous & H is distributive ) ) proof let H be non empty complete Poset; ::_thesis: ( H is Heyting iff ( H is meet-continuous & H is distributive ) ) hereby ::_thesis: ( H is meet-continuous & H is distributive implies H is Heyting ) assume A1: H is Heyting ; ::_thesis: ( H is meet-continuous & H is distributive ) then for x being Element of H holds x "/\" is lower_adjoint by WAYBEL_1:def_19; then for X being Subset of H for x being Element of H holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of H : y in X } ,H) by WAYBEL_1:64; then ( H is up-complete & H is satisfying_MC ) by Th37; hence H is meet-continuous ; ::_thesis: H is distributive thus H is distributive by A1; ::_thesis: verum end; assume A2: ( H is meet-continuous & H is distributive ) ; ::_thesis: H is Heyting thus H is LATTICE ; :: according to WAYBEL_1:def_19 ::_thesis: for b1 being Element of the carrier of H holds b1 "/\" is lower_adjoint let a be Element of H; ::_thesis: a "/\" is lower_adjoint ( ( for X being finite Subset of H holds a "/\" preserves_sup_of X ) & ( for X being non empty directed Subset of H holds a "/\" preserves_sup_of X ) ) by A2, Th17, WAYBEL_0:def_37; then a "/\" is sups-preserving by WAYBEL_0:74; hence a "/\" is lower_adjoint by WAYBEL_1:17; ::_thesis: verum end; registration cluster non empty reflexive transitive antisymmetric Heyting complete -> non empty distributive meet-continuous for RelStr ; coherence for b1 being non empty Poset st b1 is complete & b1 is Heyting holds ( b1 is meet-continuous & b1 is distributive ) by Th56; cluster non empty reflexive transitive antisymmetric distributive complete meet-continuous -> non empty Heyting for RelStr ; coherence for b1 being non empty Poset st b1 is complete & b1 is meet-continuous & b1 is distributive holds b1 is Heyting by Th56; end;