:: Introduction to Lattice Theory :: by Stanis{\l}aw \.Zukowski :: :: Received April 14, 1989 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies STRUCT_0, BINOP_1, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1, FUNCT_1, PBOOLE, XXREAL_2, CAT_1, LATTICES, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, CARD_1, STRUCT_0, BINOP_1; constructors BINOP_1, STRUCT_0; registrations XBOOLE_0, SUBSET_1, CARD_1, STRUCT_0; requirements SUBSET, BOOLE, NUMERALS; equalities STRUCT_0; expansions STRUCT_0; theorems ZFMISC_1, SUBSET_1; begin definition struct(1-sorted) /\-SemiLattStr (# carrier -> set, L_meet -> BinOp of the carrier #); end; definition struct (1-sorted) \/-SemiLattStr (# carrier -> set, L_join -> BinOp of the carrier #); end; definition struct (/\-SemiLattStr,\/-SemiLattStr) LattStr (# carrier -> set, L_join, L_meet -> BinOp of the carrier #); end; registration let D be non empty set, u be BinOp of D; cluster \/-SemiLattStr (# D, u #) -> non empty; coherence; cluster /\-SemiLattStr (# D, u #) -> non empty; coherence; end; registration let D be non empty set, u,n be BinOp of D; cluster LattStr (# D, u, n #) -> non empty; coherence; end; registration cluster 1-element strict for \/-SemiLattStr; existence proof set u = the BinOp of bool {}; take L = \/-SemiLattStr (# bool {}, u #); thus thesis by ZFMISC_1:1; end; cluster 1-element strict for /\-SemiLattStr; existence proof set u = the BinOp of bool {}; take L = /\-SemiLattStr (# bool {}, u #); thus thesis by ZFMISC_1:1; end; cluster 1-element strict for LattStr; existence proof set u = the BinOp of bool {}; take L = LattStr (# bool {}, u, u #); thus thesis by ZFMISC_1:1; end; end; definition let G be non empty \/-SemiLattStr, p, q be Element of G; func p"\/"q -> Element of G equals (the L_join of G).(p,q); coherence; end; definition let G be non empty /\-SemiLattStr, p, q be Element of G; func p"/\"q -> Element of G equals (the L_meet of G).(p,q); coherence; end; definition let G be non empty \/-SemiLattStr, p, q be Element of G; pred p [= q means :Def3: p"\/"q = q; end; Lm1: for uu,nn being BinOp of bool {}, x,y being Element of LattStr(#bool {}, uu,nn#) holds x = y proof let uu,nn be BinOp of bool {}, x,y be Element of LattStr(#bool {},uu,nn#); x = {}; hence thesis; end; Lm2: for n being BinOp of bool {}, x,y being Element of \/-SemiLattStr (#bool {}, n#) holds x = y proof let n be BinOp of bool {}; let x,y be Element of \/-SemiLattStr (#bool {}, n#); x = {}; hence thesis; end; Lm3: for n being BinOp of bool {}, x,y being Element of /\-SemiLattStr (#bool {}, n#) holds x = y proof let n be BinOp of bool {}; let x,y be Element of /\-SemiLattStr (#bool {}, n#); x = {}; hence thesis; end; definition let IT be non empty \/-SemiLattStr; attr IT is join-commutative means :Def4: for a,b being Element of IT holds a "\/"b = b"\/"a; attr IT is join-associative means :Def5: for a,b,c being Element of IT holds a"\/"(b"\/"c) = (a"\/"b)"\/"c; end; definition let IT be non empty /\-SemiLattStr; attr IT is meet-commutative means :Def6: for a,b being Element of IT holds a "/\"b = b"/\"a; attr IT is meet-associative means :Def7: for a,b,c being Element of IT holds a"/\"(b"/\"c) = (a"/\"b)"/\"c; end; definition let IT be non empty LattStr; attr IT is meet-absorbing means :Def8: for a,b being Element of IT holds (a "/\"b)"\/"b = b; attr IT is join-absorbing means :Def9: for a,b being Element of IT holds a "/\"(a"\/"b)=a; end; definition let IT be non empty LattStr; attr IT is Lattice-like means IT is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing; end; registration cluster Lattice-like -> join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing for non empty LattStr; coherence; cluster join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing -> Lattice-like for non empty LattStr; coherence; end; registration cluster strict join-commutative join-associative for non empty \/-SemiLattStr; existence proof set u = the BinOp of bool {}; take GGj = \/-SemiLattStr(#bool {},u#); ( for x,y being Element of GGj holds x"\/"y = y"\/"x)& for x,y,z being Element of GGj holds x"\/"(y"\/"z) = (x"\/"y)"\/"z by Lm2; hence thesis; end; cluster strict meet-commutative meet-associative for non empty /\-SemiLattStr; existence proof set u = the BinOp of bool {}; take GGm = /\-SemiLattStr(#bool {},u#); ( for x,y being Element of GGm holds x"/\"y = y"/\"x)& for x,y,z being Element of GGm holds x"/\"(y"/\"z) = (x"/\"y)"/\"z by Lm3; hence thesis; end; cluster strict Lattice-like for non empty LattStr; existence proof set u = the BinOp of bool {}; take GG = LattStr(#bool {},u,u#); A1: ( for x,y being Element of GG holds (x"/\"y)"\/"y = y)& for x,y being Element of GG holds x"/\"y = y"/\"x by Lm1; A2: ( for x,y,z being Element of GG holds x"/\"(y"/\"z) = (x"/\"y)"/\"z)& for x,y being Element of GG holds x"/\"(x"\/"y) = x by Lm1; ( for x,y being Element of GG holds x"\/"y = y"\/"x)& for x,y,z being Element of GG holds x"\/"(y"\/"z) = (x"\/"y)"\/"z by Lm1; then GG is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A1,A2; hence thesis; end; end; definition mode Lattice is Lattice-like non empty LattStr; end; definition let L be join-commutative non empty \/-SemiLattStr, a, b be Element of L; redefine func a"\/"b; commutativity by Def4; end; definition let L be meet-commutative non empty /\-SemiLattStr, a, b be Element of L; redefine func a"/\"b; commutativity by Def6; end; definition let IT be non empty LattStr; attr IT is distributive means :Def11: for a,b,c being Element of IT holds a "/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c); end; definition let IT be non empty LattStr; attr IT is modular means for a,b,c being Element of IT st a [= c holds a"\/"(b"/\"c) = (a"\/"b)"/\"c; end; definition let IT be non empty /\-SemiLattStr; attr IT is lower-bounded means :Def13: ex c being Element of IT st for a being Element of IT holds c"/\"a = c & a"/\"c = c; end; definition let IT be non empty \/-SemiLattStr; attr IT is upper-bounded means :Def14: ex c being Element of IT st for a being Element of IT holds c"\/"a = c & a"\/"c = c; end; Lm4: for n,u being BinOp of bool {} holds LattStr (#bool {},n,u#) is Lattice proof let n,u be BinOp of bool {}; set G = LattStr (#bool {},n,u#); for x,y,z being Element of G holds x"\/"(y"\/"z) = (x"\/"y)"\/"z by Lm1; then A1: G is join-associative; for x,y being Element of G holds (x"/\"y)"\/"y = y by Lm1; then A2: G is meet-absorbing; for x,y being Element of G holds x"/\"(x"\/"y) = x by Lm1; then A3: G is join-absorbing; for x,y,z being Element of G holds x"/\"(y"/\"z) = (x"/\"y)"/\"z by Lm1; then A4: G is meet-associative; for x,y being Element of G holds x"/\"y = y"/\"x by Lm1; then A5: G is meet-commutative; for x,y being Element of G holds x"\/"y = y"\/"x by Lm1; then G is join-commutative; hence thesis by A1,A2,A5,A4,A3; end; registration cluster strict distributive lower-bounded upper-bounded modular for Lattice; existence proof set uu = the BinOp of bool {}; set GG=LattStr(#bool {},uu,uu#); reconsider GG as Lattice by Lm4; reconsider 0GG={}, D = {} as Element of GG by ZFMISC_1:def 1; for x being Element of GG holds 0GG"/\"x = 0GG & x"/\"0GG = 0GG; then A1: GG is lower-bounded; for x being Element of GG holds D"\/"x = D & x"\/"D = D; then A2: GG is upper-bounded; for x,y,z being Element of GG holds x"/\"(y"\/"z) = (x"/\"y)"\/"(x"/\" z) by Lm1; then A3: GG is distributive; for x,y,z being Element of GG holds x [= z implies x"\/"(y"/\"z) = (x "\/"y)"/\"z by Lm1; then GG is modular; hence thesis by A1,A3,A2; end; end; definition mode D_Lattice is distributive Lattice; mode M_Lattice is modular Lattice; mode 0_Lattice is lower-bounded Lattice; mode 1_Lattice is upper-bounded Lattice; end; Lm5: for n,u being BinOp of bool {} holds LattStr (#bool {},n,u#) is 0_Lattice proof let n,u be BinOp of bool {}; set G = LattStr (#bool {},n,u#); reconsider G as Lattice by Lm4; reconsider D={} as Element of G by ZFMISC_1:def 1; for x being Element of G holds D"/\"x = D & x"/\"D = D; hence thesis by Def13; end; Lm6: for n,u being BinOp of bool {} holds LattStr (#bool {},n,u#) is 1_Lattice proof let n,u be BinOp of bool {}; set G = LattStr (#bool {},n,u#); reconsider G as Lattice by Lm4; reconsider D={} as Element of G by ZFMISC_1:def 1; for x being Element of G holds D"\/"x = D & x"\/"D = D; hence thesis by Def14; end; definition let IT be non empty LattStr; attr IT is bounded means IT is lower-bounded upper-bounded; end; registration cluster lower-bounded upper-bounded -> bounded for non empty LattStr; coherence; cluster bounded -> lower-bounded upper-bounded for non empty LattStr; coherence; end; registration cluster bounded strict for Lattice; existence proof set uu = the BinOp of bool {}; set G=LattStr(#bool {},uu,uu#); reconsider G as Lattice by Lm4; G is 0_Lattice & G is 1_Lattice by Lm5,Lm6; hence thesis; end; end; definition mode 01_Lattice is bounded Lattice; end; definition let L be non empty /\-SemiLattStr; assume A1: L is lower-bounded; func Bottom L -> Element of L means :Def16: for a being Element of L holds it "/\" a = it & a "/\" it = it; existence by A1; uniqueness proof let c1,c2 be Element of L such that A2: for a being Element of L holds c1"/\"a = c1 & a"/\"c1 = c1 and A3: for a being Element of L holds c2"/\"a = c2 & a"/\"c2 = c2; thus c1 = c2"/\"c1 by A2 .= c2 by A3; end; end; definition let L be non empty \/-SemiLattStr; assume A1: L is upper-bounded; func Top L -> Element of L means :Def17: for a being Element of L holds it "\/" a = it & a "\/" it = it; existence by A1; uniqueness proof let c1,c2 be Element of L such that A2: for a being Element of L holds c1"\/"a = c1 & a"\/"c1 = c1 and A3: for a being Element of L holds c2"\/"a = c2 & a"\/"c2 = c2; thus c1 = c2"\/"c1 by A2 .= c2 by A3; end; end; definition let L be non empty LattStr, a, b be Element of L; pred a is_a_complement_of b means a"\/"b = Top L & b"\/"a = Top L & a"/\"b = Bottom L & b"/\"a = Bottom L; end; definition let IT be non empty LattStr; attr IT is complemented means :Def19: for b being Element of IT ex a being Element of IT st a is_a_complement_of b; end; registration cluster bounded complemented strict for Lattice; existence proof set n = the BinOp of bool {}; reconsider GG = LattStr (#bool {},n,n#) as strict Lattice by Lm4; take GG; GG is 0_Lattice & GG is 1_Lattice by Lm5,Lm6; hence GG is bounded; thus GG is complemented proof set a = the Element of GG; let b be Element of GG; take a; thus a"\/"b = Top GG & b"\/"a = Top GG by Lm1; thus a"/\"b = Bottom GG & b"/\"a = Bottom GG by Lm1; end; thus thesis; end; end; definition mode C_Lattice is complemented 01_Lattice; end; definition let IT be non empty LattStr; attr IT is Boolean means IT is bounded complemented distributive; end; registration cluster Boolean -> bounded complemented distributive for non empty LattStr; coherence; cluster bounded complemented distributive -> Boolean for non empty LattStr; coherence; end; registration cluster Boolean strict for Lattice; existence proof set n = the BinOp of bool {}; reconsider G = LattStr (#bool {},n,n#) as strict Lattice by Lm4; A1: G is complemented proof let b be Element of G; take b; thus b"\/"b = Top G & b"\/"b = Top G by Lm1; thus b"/\"b = Bottom G & b"/\"b = Bottom G by Lm1; end; G is 0_Lattice & G is 1_Lattice by Lm5,Lm6; then reconsider G as C_Lattice by A1; for x,y,z being Element of G holds x"/\"(y"\/"z) = (x"/\"y)"\/"(x"/\"z ) by Lm1; then G is distributive; hence thesis; end; end; definition mode B_Lattice is Boolean Lattice; end; registration let L be meet-absorbing join-absorbing meet-commutative non empty LattStr, a be Element of L; reduce a "\/" a to a; reducibility proof thus a"\/"a = ( a "/\" ( a"\/"a ) ) "\/" a by Def9 .= a by Def8; end; end; registration let L be meet-absorbing join-absorbing meet-commutative non empty LattStr, a be Element of L; reduce a "/\" a to a; reducibility proof a"/\"( a"\/"a ) = a by Def9; hence thesis; end; end; ::\$CT 2 theorem Th1: for L being Lattice holds (for a,b,c being Element of L holds a "/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c)) iff for a,b,c being Element of L holds a "\/"(b"/\"c) = (a"\/"b)"/\"(a"\/"c) proof let L be Lattice; hereby assume A1: for a,b,c be Element of L holds a"/\"(b"\/"c)=(a"/\"b)"\/"(a"/\"c); let a,b,c be Element of L; thus a"\/"(b"/\"c)=(a"\/"(c"/\"a))"\/"(c"/\"b) by Def8 .=a"\/"((c"/\"a)"\/"(c"/\"b)) by Def5 .=a"\/"((a"\/"b)"/\"c) by A1 .=((a"\/"b)"/\"a)"\/"((a"\/"b)"/\"c) by Def9 .=(a"\/"b)"/\"(a"\/"c) by A1; end; assume A2: for a,b,c be Element of L holds a"\/"(b"/\"c)=(a"\/"b)"/\"(a"\/"c); let a,b,c be Element of L; thus a"/\"(b"\/"c)=(a"/\"(c"\/"a))"/\"(c"\/"b) by Def9 .=a"/\"((c"\/"a)"/\"(c"\/"b)) by Def7 .=a"/\"((a"/\"b)"\/"c) by A2 .=((a"/\"b)"\/"a)"/\"((a"/\"b)"\/"c) by Def8 .=(a"/\"b)"\/"(a"/\"c) by A2; end; theorem Th2: for L being meet-absorbing join-absorbing non empty LattStr, a , b being Element of L holds a [= b iff a"/\"b = a by Def8,Def9; theorem Th3: for L being meet-absorbing join-absorbing join-associative meet-commutative non empty LattStr, a, b being Element of L holds a [= a"\/"b proof let L be meet-absorbing join-absorbing join-associative meet-commutative non empty LattStr, a, b be Element of L; thus a"\/"( a"\/"b) = (a"\/"a)"\/"b by Def5 .= a"\/"b; end; theorem Th4: for L being meet-absorbing meet-commutative non empty LattStr, a, b being Element of L holds a"/\"b [= a by Def8; definition let L be meet-absorbing join-absorbing meet-commutative non empty LattStr, a, b be Element of L; redefine pred a [= b; reflexivity; end; theorem for L being join-associative non empty \/-SemiLattStr, a, b, c being Element of L holds a [= b & b [= c implies a [= c by Def5; theorem Th6: for L being join-commutative non empty \/-SemiLattStr, a, b being Element of L holds a [= b & b [= a implies a=b proof let L be join-commutative non empty \/-SemiLattStr, a, b be Element of L; assume a"\/"b = b & b"\/"a =a; hence thesis; end; theorem Th7: for L being meet-absorbing join-absorbing meet-associative non empty LattStr, a, b, c being Element of L holds a [= b implies a"/\"c [= b"/\" c proof let L be meet-absorbing join-absorbing meet-associative non empty LattStr, a, b, c be Element of L; assume a [= b; hence (a"/\"c)"\/"(b"/\"c) = ((a"/\"b)"/\"c)"\/"(b"/\"c) by Th2 .= (a"/\"(b"/\"c))"\/"(b"/\"c) by Def7 .= b"/\"c by Def8; end; theorem for L being Lattice holds (for a,b,c being Element of L holds (a"/\"b) "\/"(b"/\"c)"\/"(c"/\"a) = (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a)) implies L is distributive proof let L be Lattice; assume A1: for a,b,c being Element of L holds (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) = (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a); A2: now let a,b,c be Element of L; assume A3: c [= a; thus a"/\"(b"\/"c) = (b"\/"c)"/\"(a"/\"(a"\/"b)) by Def9 .= (a"\/"b)"/\"((b"\/"c)"/\"a) by Def7 .= (a"\/"b)"/\"((b"\/"c)"/\"(c"\/"a)) by A3 .= (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) by Def7 .= (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) by A1 .= (a"/\"b)"\/"((b"/\"c)"\/"(c"/\"a)) by Def5 .= (a"/\"b)"\/"((b"/\"c)"\/"c) by A3,Th2 .= (a"/\"b)"\/"c by Def8; end; let a,b,c be Element of L; A4: ((a"/\"b)"\/"(c"/\"a))"\/"a = (a"/\"b)"\/"((c"/\"a)"\/"a) by Def5 .= (a"/\"b)"\/"a by Def8 .= a by Def8; thus a"/\"(b"\/"c) = (a"/\"(c"\/"a))"/\"(b"\/"c) by Def9 .= a"/\"((c"\/"a)"/\"(b"\/"c)) by Def7 .= (a"/\"(a"\/"b))"/\"((c"\/"a)"/\"(b"\/"c)) by Def9 .= a"/\"((a"\/"b)"/\"((b"\/"c)"/\"(c"\/"a))) by Def7 .= a"/\"((a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a)) by Def7 .= a"/\"((b"/\"c)"\/"(a"/\"b)"\/"(c"/\"a)) by A1 .= a"/\"((b"/\"c)"\/"((a"/\"b)"\/"(c"/\"a))) by Def5 .= (a"/\"(b"/\"c))"\/"((a"/\"b)"\/"(c"/\"a)) by A2,A4,Def3 .= (a"/\"b"/\"c)"\/"((a"/\"b)"\/"(c"/\"a)) by Def7 .= ((a"/\"b"/\"c)"\/"(a"/\"b))"\/"(c"/\"a) by Def5 .= (a"/\"b)"\/"(a"/\"c) by Def8; end; reserve L for D_Lattice; reserve a, b, c for Element of L; theorem Th9: a"\/"(b"/\"c) = (a"\/"b)"/\"(a"\/"c) proof for a,b,c holds a"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c) by Def11; hence thesis by Th1; end; theorem Th10: c"/\"a = c"/\"b & c"\/"a = c"\/"b implies a=b proof assume that A1: c"/\"a = c"/\"b and A2: c"\/"a = c"\/"b; thus a = a"/\"( c"\/"a ) by Def9 .= ( b"/\"c )"\/"( b"/\"a ) by A1,A2,Def11 .= b"/\"( c"\/"a ) by Def11 .= b by A2,Def9; end; theorem (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) = (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) proof thus (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) = (((a"\/"b)"/\"(b"\/"c))"/\"c)"\/"((( a"\/"b)"/\"(b"\/"c))"/\"a) by Def11 .= ((a"\/"b)"/\"((b"\/"c)"/\"c))"\/"(((a"\/"b)"/\"(b"\/"c))"/\"a) by Def7 .= ((a"\/"b)"/\"c)"\/"(a"/\"((a"\/"b)"/\"(b"\/"c))) by Def9 .= ((a"\/"b)"/\"c)"\/"((a"/\"(a"\/"b))"/\"(b"\/"c)) by Def7 .= (c"/\"(a"\/"b))"\/"(a"/\"(b"\/"c)) by Def9 .= ((c"/\"a)"\/"(c"/\"b))"\/"(a"/\"(b"\/"c)) by Def11 .= ((a"/\"b)"\/"(c"/\"a))"\/"((c"/\"a)"\/"(b"/\"c)) by Def11 .= (a"/\"b)"\/"((c"/\"a)"\/"((c"/\"a)"\/"(b"/\"c))) by Def5 .= (a"/\"b)"\/"(((c"/\"a)"\/"(c"/\"a))"\/"(b"/\"c)) by Def5 .= (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) by Def5; end; registration cluster distributive -> modular for Lattice; coherence proof let L be Lattice; assume A1: L is distributive; let a,b,c be Element of L; assume a"\/"c = c; hence a"\/"(b"/\"c) = (a"\/"b)"/\"c by A1,Th9; end; end; registration let L be 0_Lattice, a be Element of L; reduce Bottom L "\/" a to a; reducibility proof thus Bottom L"\/"a = ( Bottom L"/\"a )"\/"a by Def16 .= a by Def8; end; reduce Bottom L "/\" a to Bottom L; reducibility by Def16; end; theorem for L being 0_Lattice, a being Element of L holds Bottom L "\/" a = a; theorem for L being 0_Lattice, a being Element of L holds Bottom L "/\" a = Bottom L; theorem for L being 0_Lattice, a being Element of L holds Bottom L [= a; registration let L be 1_Lattice, a be Element of L; reduce Top L"/\"a to a; reducibility proof thus Top L"/\"a = ( Top L"\/"a )"/\"a by Def17 .= a by Def9; end; reduce Top L"\/"a to Top L; reducibility by Def17; end; theorem for L being 1_Lattice, a being Element of L holds Top L"/\"a = a; theorem for L being 1_Lattice, a being Element of L holds Top L"\/"a = Top L; theorem for L being 1_Lattice, a being Element of L holds a [= Top L proof let L be 1_Lattice, a be Element of L; Top L"/\"a [= Top L by Th4; hence thesis; end; definition let L be non empty LattStr, x be Element of L; assume A1: L is complemented D_Lattice; func x` -> Element of L means :Def21: it is_a_complement_of x; existence by A1,Def19; uniqueness by A1,Th10; end; reserve L for B_Lattice; reserve a, b for Element of L; theorem Th18: a`"/\"a = Bottom L proof a` is_a_complement_of a by Def21; hence thesis; end; theorem Th19: a`"\/"a = Top L proof a` is_a_complement_of a by Def21; hence thesis; end; registration let L,a; reduce a`` to a; reducibility proof a` is_a_complement_of a by Def21; then A1: a"\/"a` =Top L & a "/\"a`= Bottom L; a`` is_a_complement_of a` by Def21; then a``"\/"a` = Top L & a``"/\"a` = Bottom L; hence thesis by A1,Th10; end; end; theorem a`` = a; theorem Th21: ( a"/\"b )` = a`"\/" b` proof A1: (a`"\/"b`)"/\"(a"/\"b) = (a"/\"b)"/\"(a`"\/"b`) & (a`"\/"b`)"\/"(a"/\"b) = (a"/\"b)"\/"(a`"\/"b`); A2: (a`"\/"b`)"/\"(a"/\"b) = ((a`"\/"b`)"/\"a)"/\"b by Def7 .= ((a`"/\"a)"\/"(b`"/\"a))"/\"b by Def11 .= (Bottom L"\/"(b`"/\"a))"/\"b by Th18 .= (b"/\"b`)"/\"a by Def7 .= Bottom L"/\"a by Th18 .= Bottom L; (a`"\/"b`)"\/"(a"/\"b) = a`"\/"(b`"\/"(a"/\"b)) by Def5 .= a`"\/"((b`"\/"a)"/\"(b`"\/"b)) by Th9 .= a`"\/"((b`"\/"a)"/\"Top L) by Th19 .= b`"\/"(a"\/"a`) by Def5 .= b`"\/"Top L by Th19 .= Top L; then a`"\/"b` is_a_complement_of a"/\"b by A1,A2; hence thesis by Def21; end; theorem ( a"\/"b )` = a`"/\" b` proof thus (a"\/"b)` = (a``"\/"b``)` .= (a`"/\"b`)`` by Th21 .= a`"/\"b`; end; theorem Th23: b"/\"a = Bottom L iff b [= a` proof thus b"/\"a = Bottom L implies b [= a` proof assume A1: b"/\"a = Bottom L; b = b"/\"Top L .= b"/\"(a"\/"a`) by Th19 .= Bottom L"\/"(b"/\"a`) by A1,Def11 .= b"/\"a`; then b"\/"a` = a` by Def8; hence thesis; end; thus thesis proof assume b [= a`; then b"/\"a [= a`"/\"a by Th7; then A2: b"/\"a [= Bottom L by Th18; Bottom L [= b"/\"a; hence thesis by A2,Th6; end; end; theorem a [= b implies b` [= a` proof assume a [= b; then b`"/\"a [= b`"/\"b by Th7; then A1: b`"/\"a [= Bottom L by Th18; Bottom L [= b`"/\"a; then b `"/\"a = Bottom L by A1,Th6; hence thesis by Th23; end; begin :: Addenda :: missing, 2009.07.28, A.T. definition let L be Lattice, S be Subset of L; attr S is initial means :Def22: for p,q being Element of L st p [= q & q in S holds p in S; attr S is final means :Def23: for p,q being Element of L st p [= q & p in S holds q in S; attr S is meet-closed means for p,q being Element of L st p in S & q in S holds p "/\" q in S; attr S is join-closed means for p,q being Element of L st p in S & q in S holds p "\/" q in S; end; registration let L be Lattice; cluster [#]L -> initial final non empty; coherence; end; registration let L be Lattice; cluster initial final non empty for Subset of L; existence proof take [#]L; thus thesis; end; cluster empty -> initial final for Subset of L; coherence; cluster initial -> meet-closed for Subset of L; coherence by Th4; cluster final -> join-closed for Subset of L; coherence by Th3; end; theorem for L being Lattice, S being initial final non empty Subset of L holds S = [#]L proof let L be Lattice, S be initial final non empty Subset of L; consider p being Element of L such that A1: p in S by SUBSET_1:4; for x being Element of L holds x in S iff x in [#]L proof let x be Element of L; thus x in S implies x in [#]L; assume x in [#]L; A2: x "/\" p in S by A1,Def22,Th4; thus x in S by A2,Def23,Th4; end; hence S = [#]L by SUBSET_1:3; end;