:: LATTICES semantic presentation begin definition attrc1 is strict ; struct /\-SemiLattStr -> 1-sorted ; aggr/\-SemiLattStr(# carrier, L_meet #) -> /\-SemiLattStr ; sel L_meet c1 -> BinOp of the carrier of c1; end; definition attrc1 is strict ; struct \/-SemiLattStr -> 1-sorted ; aggr\/-SemiLattStr(# carrier, L_join #) -> \/-SemiLattStr ; sel L_join c1 -> BinOp of the carrier of c1; end; definition attrc1 is strict ; struct LattStr -> /\-SemiLattStr , \/-SemiLattStr ; aggrLattStr(# carrier, L_join, L_meet #) -> LattStr ; end; registration let D be non empty set ; let u be BinOp of D; cluster \/-SemiLattStr(# D,u #) -> non empty ; coherence not \/-SemiLattStr(# D,u #) is empty ; cluster /\-SemiLattStr(# D,u #) -> non empty ; coherence not /\-SemiLattStr(# D,u #) is empty ; end; registration let D be non empty set ; let u, n be BinOp of D; cluster LattStr(# D,u,n #) -> non empty ; coherence not LattStr(# D,u,n #) is empty ; end; registration cluster1 -element strict for \/-SemiLattStr ; existence ex b1 being \/-SemiLattStr st ( b1 is 1 -element & b1 is strict ) proof set u = the BinOp of (bool {}); take L = \/-SemiLattStr(# (bool {}), the BinOp of (bool {}) #); ::_thesis: ( L is 1 -element & L is strict ) thus ( L is 1 -element & L is strict ) by STRUCT_0:def_19, ZFMISC_1:1; ::_thesis: verum end; cluster1 -element strict for /\-SemiLattStr ; existence ex b1 being /\-SemiLattStr st ( b1 is 1 -element & b1 is strict ) proof set u = the BinOp of (bool {}); take L = /\-SemiLattStr(# (bool {}), the BinOp of (bool {}) #); ::_thesis: ( L is 1 -element & L is strict ) thus ( L is 1 -element & L is strict ) by STRUCT_0:def_19, ZFMISC_1:1; ::_thesis: verum end; cluster1 -element strict for LattStr ; existence ex b1 being LattStr st ( b1 is 1 -element & b1 is strict ) proof set u = the BinOp of (bool {}); take L = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #); ::_thesis: ( L is 1 -element & L is strict ) thus ( L is 1 -element & L is strict ) by STRUCT_0:def_19, ZFMISC_1:1; ::_thesis: verum end; end; definition let G be non empty \/-SemiLattStr ; let p, q be Element of G; funcp "\/" q -> Element of G equals :: LATTICES:def 1 the L_join of G . (p,q); coherence the L_join of G . (p,q) is Element of G ; end; :: deftheorem defines "\/" LATTICES:def_1_:_ for G being non empty \/-SemiLattStr for p, q being Element of G holds p "\/" q = the L_join of G . (p,q); definition let G be non empty /\-SemiLattStr ; let p, q be Element of G; funcp "/\" q -> Element of G equals :: LATTICES:def 2 the L_meet of G . (p,q); coherence the L_meet of G . (p,q) is Element of G ; end; :: deftheorem defines "/\" LATTICES:def_2_:_ for G being non empty /\-SemiLattStr for p, q being Element of G holds p "/\" q = the L_meet of G . (p,q); definition let G be non empty \/-SemiLattStr ; let p, q be Element of G; predp [= q means :Def3: :: LATTICES:def 3 p "\/" q = q; end; :: deftheorem Def3 defines [= LATTICES:def_3_:_ for G being non empty \/-SemiLattStr for p, q being Element of G holds ( p [= q iff p "\/" q = q ); Lm1: for uu, nn being BinOp of (bool {}) for x, y being Element of LattStr(# (bool {}),uu,nn #) holds x = y proof let uu, nn be BinOp of (bool {}); ::_thesis: for x, y being Element of LattStr(# (bool {}),uu,nn #) holds x = y let x, y be Element of LattStr(# (bool {}),uu,nn #); ::_thesis: x = y x = {} ; hence x = y ; ::_thesis: verum end; Lm2: for n being BinOp of (bool {}) for x, y being Element of \/-SemiLattStr(# (bool {}),n #) holds x = y proof let n be BinOp of (bool {}); ::_thesis: for x, y being Element of \/-SemiLattStr(# (bool {}),n #) holds x = y let x, y be Element of \/-SemiLattStr(# (bool {}),n #); ::_thesis: x = y x = {} ; hence x = y ; ::_thesis: verum end; Lm3: for n being BinOp of (bool {}) for x, y being Element of /\-SemiLattStr(# (bool {}),n #) holds x = y proof let n be BinOp of (bool {}); ::_thesis: for x, y being Element of /\-SemiLattStr(# (bool {}),n #) holds x = y let x, y be Element of /\-SemiLattStr(# (bool {}),n #); ::_thesis: x = y x = {} ; hence x = y ; ::_thesis: verum end; definition let IT be non empty \/-SemiLattStr ; attrIT is join-commutative means :Def4: :: LATTICES:def 4 for a, b being Element of IT holds a "\/" b = b "\/" a; attrIT is join-associative means :Def5: :: LATTICES:def 5 for a, b, c being Element of IT holds a "\/" (b "\/" c) = (a "\/" b) "\/" c; end; :: deftheorem Def4 defines join-commutative LATTICES:def_4_:_ for IT being non empty \/-SemiLattStr holds ( IT is join-commutative iff for a, b being Element of IT holds a "\/" b = b "\/" a ); :: deftheorem Def5 defines join-associative LATTICES:def_5_:_ for IT being non empty \/-SemiLattStr holds ( IT is join-associative iff for a, b, c being Element of IT holds a "\/" (b "\/" c) = (a "\/" b) "\/" c ); definition let IT be non empty /\-SemiLattStr ; attrIT is meet-commutative means :Def6: :: LATTICES:def 6 for a, b being Element of IT holds a "/\" b = b "/\" a; attrIT is meet-associative means :Def7: :: LATTICES:def 7 for a, b, c being Element of IT holds a "/\" (b "/\" c) = (a "/\" b) "/\" c; end; :: deftheorem Def6 defines meet-commutative LATTICES:def_6_:_ for IT being non empty /\-SemiLattStr holds ( IT is meet-commutative iff for a, b being Element of IT holds a "/\" b = b "/\" a ); :: deftheorem Def7 defines meet-associative LATTICES:def_7_:_ for IT being non empty /\-SemiLattStr holds ( IT is meet-associative iff for a, b, c being Element of IT holds a "/\" (b "/\" c) = (a "/\" b) "/\" c ); definition let IT be non empty LattStr ; attrIT is meet-absorbing means :Def8: :: LATTICES:def 8 for a, b being Element of IT holds (a "/\" b) "\/" b = b; attrIT is join-absorbing means :Def9: :: LATTICES:def 9 for a, b being Element of IT holds a "/\" (a "\/" b) = a; end; :: deftheorem Def8 defines meet-absorbing LATTICES:def_8_:_ for IT being non empty LattStr holds ( IT is meet-absorbing iff for a, b being Element of IT holds (a "/\" b) "\/" b = b ); :: deftheorem Def9 defines join-absorbing LATTICES:def_9_:_ for IT being non empty LattStr holds ( IT is join-absorbing iff for a, b being Element of IT holds a "/\" (a "\/" b) = a ); definition let IT be non empty LattStr ; attrIT is Lattice-like means :Def10: :: LATTICES:def 10 ( IT is join-commutative & IT is join-associative & IT is meet-absorbing & IT is meet-commutative & IT is meet-associative & IT is join-absorbing ); end; :: deftheorem Def10 defines Lattice-like LATTICES:def_10_:_ for IT being non empty LattStr holds ( IT is Lattice-like iff ( IT is join-commutative & IT is join-associative & IT is meet-absorbing & IT is meet-commutative & IT is meet-associative & IT is join-absorbing ) ); registration cluster non empty Lattice-like -> non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing for LattStr ; coherence for b1 being non empty LattStr st b1 is Lattice-like holds ( b1 is join-commutative & b1 is join-associative & b1 is meet-absorbing & b1 is meet-commutative & b1 is meet-associative & b1 is join-absorbing ) by Def10; cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing -> non empty Lattice-like for LattStr ; coherence for b1 being non empty LattStr st b1 is join-commutative & b1 is join-associative & b1 is meet-absorbing & b1 is meet-commutative & b1 is meet-associative & b1 is join-absorbing holds b1 is Lattice-like by Def10; end; registration cluster non empty strict join-commutative join-associative for \/-SemiLattStr ; existence ex b1 being non empty \/-SemiLattStr st ( b1 is strict & b1 is join-commutative & b1 is join-associative ) proof set u = the BinOp of (bool {}); take GGj = \/-SemiLattStr(# (bool {}), the BinOp of (bool {}) #); ::_thesis: ( GGj is strict & GGj is join-commutative & GGj is join-associative ) ( ( 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 ( GGj is strict & GGj is join-commutative & GGj is join-associative ) by Def4, Def5; ::_thesis: verum end; cluster non empty strict meet-commutative meet-associative for /\-SemiLattStr ; existence ex b1 being non empty /\-SemiLattStr st ( b1 is strict & b1 is meet-commutative & b1 is meet-associative ) proof set u = the BinOp of (bool {}); take GGm = /\-SemiLattStr(# (bool {}), the BinOp of (bool {}) #); ::_thesis: ( GGm is strict & GGm is meet-commutative & GGm is meet-associative ) ( ( 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 ( GGm is strict & GGm is meet-commutative & GGm is meet-associative ) by Def6, Def7; ::_thesis: verum end; cluster non empty strict Lattice-like for LattStr ; existence ex b1 being non empty LattStr st ( b1 is strict & b1 is Lattice-like ) proof set u = the BinOp of (bool {}); take GG = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #); ::_thesis: ( GG is strict & GG is Lattice-like ) 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 & GG is join-associative & GG is meet-absorbing & GG is meet-commutative & GG is meet-associative & GG is join-absorbing ) by A1, A2, Def4, Def5, Def6, Def7, Def8, Def9; hence ( GG is strict & GG is Lattice-like ) ; ::_thesis: verum end; end; definition mode Lattice is non empty Lattice-like LattStr ; end; definition let L be non empty join-commutative \/-SemiLattStr ; let a, b be Element of L; :: original: "\/" redefine funca "\/" b -> Element of L; commutativity for a, b being Element of L holds a "\/" b = b "\/" a by Def4; end; definition let L be non empty meet-commutative /\-SemiLattStr ; let a, b be Element of L; :: original: "/\" redefine funca "/\" b -> Element of L; commutativity for a, b being Element of L holds a "/\" b = b "/\" a by Def6; end; definition let IT be non empty LattStr ; attrIT is distributive means :Def11: :: LATTICES:def 11 for a, b, c being Element of IT holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c); end; :: deftheorem Def11 defines distributive LATTICES:def_11_:_ for IT being non empty LattStr holds ( IT is distributive iff for a, b, c being Element of IT holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) ); definition let IT be non empty LattStr ; attrIT is modular means :Def12: :: LATTICES:def 12 for a, b, c being Element of IT st a [= c holds a "\/" (b "/\" c) = (a "\/" b) "/\" c; end; :: deftheorem Def12 defines modular LATTICES:def_12_:_ for IT being non empty LattStr holds ( IT is modular iff for a, b, c being Element of IT st a [= c holds a "\/" (b "/\" c) = (a "\/" b) "/\" c ); definition let IT be non empty /\-SemiLattStr ; attrIT is lower-bounded means :Def13: :: LATTICES:def 13 ex c being Element of IT st for a being Element of IT holds ( c "/\" a = c & a "/\" c = c ); end; :: deftheorem Def13 defines lower-bounded LATTICES:def_13_:_ for IT being non empty /\-SemiLattStr holds ( IT is lower-bounded iff ex c being Element of IT st for a being Element of IT holds ( c "/\" a = c & a "/\" c = c ) ); definition let IT be non empty \/-SemiLattStr ; attrIT is upper-bounded means :Def14: :: LATTICES:def 14 ex c being Element of IT st for a being Element of IT holds ( c "\/" a = c & a "\/" c = c ); end; :: deftheorem Def14 defines upper-bounded LATTICES:def_14_:_ for IT being non empty \/-SemiLattStr holds ( IT is upper-bounded iff ex c being Element of IT st for a being Element of IT holds ( c "\/" a = c & a "\/" c = c ) ); Lm4: for n, u being BinOp of (bool {}) holds LattStr(# (bool {}),n,u #) is Lattice proof let n, u be BinOp of (bool {}); ::_thesis: LattStr(# (bool {}),n,u #) is Lattice set G = LattStr(# (bool {}),n,u #); for x, y, z being Element of LattStr(# (bool {}),n,u #) holds x "\/" (y "\/" z) = (x "\/" y) "\/" z by Lm1; then A1: LattStr(# (bool {}),n,u #) is join-associative by Def5; for x, y being Element of LattStr(# (bool {}),n,u #) holds (x "/\" y) "\/" y = y by Lm1; then A2: LattStr(# (bool {}),n,u #) is meet-absorbing by Def8; for x, y being Element of LattStr(# (bool {}),n,u #) holds x "/\" (x "\/" y) = x by Lm1; then A3: LattStr(# (bool {}),n,u #) is join-absorbing by Def9; for x, y, z being Element of LattStr(# (bool {}),n,u #) holds x "/\" (y "/\" z) = (x "/\" y) "/\" z by Lm1; then A4: LattStr(# (bool {}),n,u #) is meet-associative by Def7; for x, y being Element of LattStr(# (bool {}),n,u #) holds x "/\" y = y "/\" x by Lm1; then A5: LattStr(# (bool {}),n,u #) is meet-commutative by Def6; for x, y being Element of LattStr(# (bool {}),n,u #) holds x "\/" y = y "\/" x by Lm1; then LattStr(# (bool {}),n,u #) is join-commutative by Def4; hence LattStr(# (bool {}),n,u #) is Lattice by A1, A2, A5, A4, A3; ::_thesis: verum end; registration cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded for LattStr ; existence ex b1 being Lattice st ( b1 is strict & b1 is distributive & b1 is lower-bounded & b1 is upper-bounded & b1 is modular ) proof set uu = the BinOp of (bool {}); set GG = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #); reconsider GG = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #) 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 by Def13; for x being Element of GG holds ( D "\/" x = D & x "\/" D = D ) ; then A2: GG is upper-bounded by Def14; for x, y, z being Element of GG holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by Lm1; then A3: GG is distributive by Def11; for x, y, z being Element of GG st x [= z holds x "\/" (y "/\" z) = (x "\/" y) "/\" z by Lm1; then GG is modular by Def12; hence ex b1 being Lattice st ( b1 is strict & b1 is distributive & b1 is lower-bounded & b1 is upper-bounded & b1 is modular ) by A1, A3, A2; ::_thesis: verum 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 {}); ::_thesis: LattStr(# (bool {}),n,u #) is 0_Lattice set G = LattStr(# (bool {}),n,u #); reconsider G = LattStr(# (bool {}),n,u #) 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 LattStr(# (bool {}),n,u #) is 0_Lattice by Def13; ::_thesis: verum 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 {}); ::_thesis: LattStr(# (bool {}),n,u #) is 1_Lattice set G = LattStr(# (bool {}),n,u #); reconsider G = LattStr(# (bool {}),n,u #) 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 LattStr(# (bool {}),n,u #) is 1_Lattice by Def14; ::_thesis: verum end; definition let IT be non empty LattStr ; attrIT is bounded means :Def15: :: LATTICES:def 15 ( IT is lower-bounded & IT is upper-bounded ); end; :: deftheorem Def15 defines bounded LATTICES:def_15_:_ for IT being non empty LattStr holds ( IT is bounded iff ( IT is lower-bounded & IT is upper-bounded ) ); registration cluster non empty lower-bounded upper-bounded -> non empty bounded for LattStr ; coherence for b1 being non empty LattStr st b1 is lower-bounded & b1 is upper-bounded holds b1 is bounded by Def15; cluster non empty bounded -> non empty lower-bounded upper-bounded for LattStr ; coherence for b1 being non empty LattStr st b1 is bounded holds ( b1 is lower-bounded & b1 is upper-bounded ) by Def15; end; registration cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like bounded for LattStr ; existence ex b1 being Lattice st ( b1 is bounded & b1 is strict ) proof set uu = the BinOp of (bool {}); set G = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #); reconsider G = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #) as Lattice by Lm4; ( G is 0_Lattice & G is 1_Lattice ) by Lm5, Lm6; hence ex b1 being Lattice st ( b1 is bounded & b1 is strict ) ; ::_thesis: verum 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: :: LATTICES:def 16 for a being Element of L holds ( it "/\" a = it & a "/\" it = it ); existence ex b1 being Element of L st for a being Element of L holds ( b1 "/\" a = b1 & a "/\" b1 = b1 ) by A1, Def13; uniqueness for b1, b2 being Element of L st ( for a being Element of L holds ( b1 "/\" a = b1 & a "/\" b1 = b1 ) ) & ( for a being Element of L holds ( b2 "/\" a = b2 & a "/\" b2 = b2 ) ) holds b1 = b2 proof let c1, c2 be Element of L; ::_thesis: ( ( for a being Element of L holds ( c1 "/\" a = c1 & a "/\" c1 = c1 ) ) & ( for a being Element of L holds ( c2 "/\" a = c2 & a "/\" c2 = c2 ) ) implies c1 = c2 ) assume 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 ) ; ::_thesis: c1 = c2 thus c1 = c2 "/\" c1 by A2 .= c2 by A3 ; ::_thesis: verum end; end; :: deftheorem Def16 defines Bottom LATTICES:def_16_:_ for L being non empty /\-SemiLattStr st L is lower-bounded holds for b2 being Element of L holds ( b2 = Bottom L iff for a being Element of L holds ( b2 "/\" a = b2 & a "/\" b2 = b2 ) ); definition let L be non empty \/-SemiLattStr ; assume A1: L is upper-bounded ; func Top L -> Element of L means :Def17: :: LATTICES:def 17 for a being Element of L holds ( it "\/" a = it & a "\/" it = it ); existence ex b1 being Element of L st for a being Element of L holds ( b1 "\/" a = b1 & a "\/" b1 = b1 ) by A1, Def14; uniqueness for b1, b2 being Element of L st ( for a being Element of L holds ( b1 "\/" a = b1 & a "\/" b1 = b1 ) ) & ( for a being Element of L holds ( b2 "\/" a = b2 & a "\/" b2 = b2 ) ) holds b1 = b2 proof let c1, c2 be Element of L; ::_thesis: ( ( for a being Element of L holds ( c1 "\/" a = c1 & a "\/" c1 = c1 ) ) & ( for a being Element of L holds ( c2 "\/" a = c2 & a "\/" c2 = c2 ) ) implies c1 = c2 ) assume 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 ) ; ::_thesis: c1 = c2 thus c1 = c2 "\/" c1 by A2 .= c2 by A3 ; ::_thesis: verum end; end; :: deftheorem Def17 defines Top LATTICES:def_17_:_ for L being non empty \/-SemiLattStr st L is upper-bounded holds for b2 being Element of L holds ( b2 = Top L iff for a being Element of L holds ( b2 "\/" a = b2 & a "\/" b2 = b2 ) ); definition let L be non empty LattStr ; let a, b be Element of L; preda is_a_complement_of b means :Def18: :: LATTICES:def 18 ( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L ); end; :: deftheorem Def18 defines is_a_complement_of LATTICES:def_18_:_ for L being non empty LattStr for a, b being Element of L holds ( a is_a_complement_of b iff ( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L ) ); definition let IT be non empty LattStr ; attrIT is complemented means :Def19: :: LATTICES:def 19 for b being Element of IT ex a being Element of IT st a is_a_complement_of b; end; :: deftheorem Def19 defines complemented LATTICES:def_19_:_ for IT being non empty LattStr holds ( IT is complemented iff for b being Element of IT ex a being Element of IT st a is_a_complement_of b ); registration cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like bounded complemented for LattStr ; existence ex b1 being Lattice st ( b1 is bounded & b1 is complemented & b1 is strict ) proof set n = the BinOp of (bool {}); reconsider GG = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #) as strict Lattice by Lm4; take GG ; ::_thesis: ( GG is bounded & GG is complemented & GG is strict ) ( GG is 0_Lattice & GG is 1_Lattice ) by Lm5, Lm6; hence GG is bounded ; ::_thesis: ( GG is complemented & GG is strict ) thus GG is complemented ::_thesis: GG is strict proof set a = the Element of GG; let b be Element of GG; :: according to LATTICES:def_19 ::_thesis: ex a being Element of GG st a is_a_complement_of b take the Element of GG ; ::_thesis: the Element of GG is_a_complement_of b thus ( the Element of GG "\/" b = Top GG & b "\/" the Element of GG = Top GG ) by Lm1; :: according to LATTICES:def_18 ::_thesis: ( the Element of GG "/\" b = Bottom GG & b "/\" the Element of GG = Bottom GG ) thus ( the Element of GG "/\" b = Bottom GG & b "/\" the Element of GG = Bottom GG ) by Lm1; ::_thesis: verum end; thus GG is strict ; ::_thesis: verum end; end; definition mode C_Lattice is complemented 01_Lattice; end; definition let IT be non empty LattStr ; attrIT is Boolean means :Def20: :: LATTICES:def 20 ( IT is bounded & IT is complemented & IT is distributive ); end; :: deftheorem Def20 defines Boolean LATTICES:def_20_:_ for IT being non empty LattStr holds ( IT is Boolean iff ( IT is bounded & IT is complemented & IT is distributive ) ); registration cluster non empty Boolean -> non empty distributive bounded complemented for LattStr ; coherence for b1 being non empty LattStr st b1 is Boolean holds ( b1 is bounded & b1 is complemented & b1 is distributive ) by Def20; cluster non empty distributive bounded complemented -> non empty Boolean for LattStr ; coherence for b1 being non empty LattStr st b1 is bounded & b1 is complemented & b1 is distributive holds b1 is Boolean by Def20; end; registration cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Boolean for LattStr ; existence ex b1 being Lattice st ( b1 is Boolean & b1 is strict ) proof set n = the BinOp of (bool {}); reconsider G = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #) as strict Lattice by Lm4; A1: G is complemented proof let b be Element of G; :: according to LATTICES:def_19 ::_thesis: ex a being Element of G st a is_a_complement_of b take b ; ::_thesis: b is_a_complement_of b thus ( b "\/" b = Top G & b "\/" b = Top G ) by Lm1; :: according to LATTICES:def_18 ::_thesis: ( b "/\" b = Bottom G & b "/\" b = Bottom G ) thus ( b "/\" b = Bottom G & b "/\" b = Bottom G ) by Lm1; ::_thesis: verum end; ( G is 0_Lattice & G is 1_Lattice ) by Lm5, Lm6; then reconsider G = 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 by Def11; hence ex b1 being Lattice st ( b1 is Boolean & b1 is strict ) ; ::_thesis: verum end; end; definition mode B_Lattice is Boolean Lattice; end; registration let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ; let a be Element of L; reducea "\/" a to a; reducibility a "\/" a = a proof thus a "\/" a = (a "/\" (a "\/" a)) "\/" a by Def9 .= a by Def8 ; ::_thesis: verum end; end; registration let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ; let a be Element of L; reducea "/\" a to a; reducibility a "/\" a = a proof a "/\" (a "\/" a) = a by Def9; hence a "/\" a = a ; ::_thesis: verum end; end; theorem :: LATTICES:1 canceled; theorem :: LATTICES:2 canceled; theorem Th3: :: LATTICES:3 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; ::_thesis: ( ( 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) ) hereby ::_thesis: ( ( for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) ) implies for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) ) assume A1: for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) ; ::_thesis: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) let a, b, c be Element of L; ::_thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) 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 ; ::_thesis: verum end; assume A2: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) ; ::_thesis: for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) let a, b, c be Element of L; ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) 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 ; ::_thesis: verum end; theorem Th4: :: LATTICES:4 for L being non empty meet-absorbing join-absorbing LattStr for a, b being Element of L holds ( a [= b iff a "/\" b = a ) proof let L be non empty meet-absorbing join-absorbing LattStr ; ::_thesis: for a, b being Element of L holds ( a [= b iff a "/\" b = a ) let a, b be Element of L; ::_thesis: ( a [= b iff a "/\" b = a ) ( a [= b iff a "\/" b = b ) by Def3; hence ( a [= b iff a "/\" b = a ) by Def8, Def9; ::_thesis: verum end; theorem Th5: :: LATTICES:5 for L being non empty join-associative meet-commutative meet-absorbing join-absorbing LattStr for a, b being Element of L holds a [= a "\/" b proof let L be non empty join-associative meet-commutative meet-absorbing join-absorbing LattStr ; ::_thesis: for a, b being Element of L holds a [= a "\/" b let a, b be Element of L; ::_thesis: a [= a "\/" b thus a "\/" (a "\/" b) = (a "\/" a) "\/" b by Def5 .= a "\/" b ; :: according to LATTICES:def_3 ::_thesis: verum end; theorem Th6: :: LATTICES:6 for L being non empty meet-commutative meet-absorbing LattStr for a, b being Element of L holds a "/\" b [= a proof let L be non empty meet-commutative meet-absorbing LattStr ; ::_thesis: for a, b being Element of L holds a "/\" b [= a let a, b be Element of L; ::_thesis: a "/\" b [= a thus (a "/\" b) "\/" a = a by Def8; :: according to LATTICES:def_3 ::_thesis: verum end; definition let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ; let a, b be Element of L; :: original: [= redefine preda [= b; reflexivity for a being Element of L holds (L,b1,b1) proof let a be Element of L; ::_thesis: (L,a,a) thus a "\/" a = a ; :: according to LATTICES:def_3 ::_thesis: verum end; end; theorem :: LATTICES:7 for L being non empty join-associative \/-SemiLattStr for a, b, c being Element of L st a [= b & b [= c holds a [= c proof let L be non empty join-associative \/-SemiLattStr ; ::_thesis: for a, b, c being Element of L st a [= b & b [= c holds a [= c let a, b, c be Element of L; ::_thesis: ( a [= b & b [= c implies a [= c ) assume ( a "\/" b = b & b "\/" c = c ) ; :: according to LATTICES:def_3 ::_thesis: a [= c hence a "\/" c = c by Def5; :: according to LATTICES:def_3 ::_thesis: verum end; theorem Th8: :: LATTICES:8 for L being non empty join-commutative \/-SemiLattStr for a, b being Element of L st a [= b & b [= a holds a = b proof let L be non empty join-commutative \/-SemiLattStr ; ::_thesis: for a, b being Element of L st a [= b & b [= a holds a = b let a, b be Element of L; ::_thesis: ( a [= b & b [= a implies a = b ) assume ( a "\/" b = b & b "\/" a = a ) ; :: according to LATTICES:def_3 ::_thesis: a = b hence a = b ; ::_thesis: verum end; theorem Th9: :: LATTICES:9 for L being non empty meet-associative meet-absorbing join-absorbing LattStr for a, b, c being Element of L st a [= b holds a "/\" c [= b "/\" c proof let L be non empty meet-associative meet-absorbing join-absorbing LattStr ; ::_thesis: for a, b, c being Element of L st a [= b holds a "/\" c [= b "/\" c let a, b, c be Element of L; ::_thesis: ( a [= b implies a "/\" c [= b "/\" c ) assume a [= b ; ::_thesis: a "/\" c [= b "/\" c hence (a "/\" c) "\/" (b "/\" c) = ((a "/\" b) "/\" c) "\/" (b "/\" c) by Th4 .= (a "/\" (b "/\" c)) "\/" (b "/\" c) by Def7 .= b "/\" c by Def8 ; :: according to LATTICES:def_3 ::_thesis: verum end; theorem :: LATTICES:10 for L being Lattice st ( for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) ) holds L is distributive proof let L be Lattice; ::_thesis: ( ( 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 ) assume A1: for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) ; ::_thesis: L is distributive A2: now__::_thesis:_for_a,_b,_c_being_Element_of_L_st_c_[=_a_holds_ a_"/\"_(b_"\/"_c)_=_(a_"/\"_b)_"\/"_c let a, b, c be Element of L; ::_thesis: ( c [= a implies a "/\" (b "\/" c) = (a "/\" b) "\/" c ) assume A3: c [= a ; ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" c 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, Def3 .= ((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, Th4 .= (a "/\" b) "\/" c by Def8 ; ::_thesis: verum end; let a, b, c be Element of L; :: according to LATTICES:def_11 ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) B4: ((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, B4, 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 ; ::_thesis: verum end; theorem Th11: :: LATTICES:11 for L being D_Lattice for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) proof let L be D_Lattice; ::_thesis: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) let a, b, c be Element of L; ::_thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by Def11; hence a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by Th3; ::_thesis: verum end; theorem Th12: :: LATTICES:12 for L being D_Lattice for c, a, b being Element of L st c "/\" a = c "/\" b & c "\/" a = c "\/" b holds a = b proof let L be D_Lattice; ::_thesis: for c, a, b being Element of L st c "/\" a = c "/\" b & c "\/" a = c "\/" b holds a = b let c, a, b be Element of L; ::_thesis: ( c "/\" a = c "/\" b & c "\/" a = c "\/" b implies a = b ) assume that A1: c "/\" a = c "/\" b and A2: c "\/" a = c "\/" b ; ::_thesis: a = 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 ; ::_thesis: verum end; theorem :: LATTICES:13 for L being D_Lattice for a, b, c being Element of L holds ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) = ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) proof let L be D_Lattice; ::_thesis: for a, b, c being Element of L holds ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) = ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) let a, b, c be Element of L; ::_thesis: ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) = ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) 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 ; ::_thesis: verum end; registration cluster non empty Lattice-like distributive -> modular for LattStr ; coherence for b1 being Lattice st b1 is distributive holds b1 is modular proof let L be Lattice; ::_thesis: ( L is distributive implies L is modular ) assume A1: L is distributive ; ::_thesis: L is modular let a, b, c be Element of L; :: according to LATTICES:def_12 ::_thesis: ( a [= c implies a "\/" (b "/\" c) = (a "\/" b) "/\" c ) assume a "\/" c = c ; :: according to LATTICES:def_3 ::_thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c hence a "\/" (b "/\" c) = (a "\/" b) "/\" c by A1, Th11; ::_thesis: verum end; end; registration let L be 0_Lattice; let a be Element of L; reduce(Bottom L) "\/" a to a; reducibility (Bottom L) "\/" a = a proof thus (Bottom L) "\/" a = ((Bottom L) "/\" a) "\/" a by Def16 .= a by Def8 ; ::_thesis: verum end; reduce(Bottom L) "/\" a to Bottom L; reducibility (Bottom L) "/\" a = Bottom L by Def16; end; theorem :: LATTICES:14 for L being 0_Lattice for a being Element of L holds (Bottom L) "\/" a = a ; theorem :: LATTICES:15 for L being 0_Lattice for a being Element of L holds (Bottom L) "/\" a = Bottom L ; theorem Th16: :: LATTICES:16 for L being 0_Lattice for a being Element of L holds Bottom L [= a proof let L be 0_Lattice; ::_thesis: for a being Element of L holds Bottom L [= a let a be Element of L; ::_thesis: Bottom L [= a Bottom L [= (Bottom L) "\/" a by Th5; hence Bottom L [= a ; ::_thesis: verum end; registration let L be 1_Lattice; let a be Element of L; reduce(Top L) "/\" a to a; reducibility (Top L) "/\" a = a proof thus (Top L) "/\" a = ((Top L) "\/" a) "/\" a by Def17 .= a by Def9 ; ::_thesis: verum end; reduce(Top L) "\/" a to Top L; reducibility (Top L) "\/" a = Top L by Def17; end; theorem :: LATTICES:17 for L being 1_Lattice for a being Element of L holds (Top L) "/\" a = a ; theorem :: LATTICES:18 for L being 1_Lattice for a being Element of L holds (Top L) "\/" a = Top L ; theorem :: LATTICES:19 for L being 1_Lattice for a being Element of L holds a [= Top L proof let L be 1_Lattice; ::_thesis: for a being Element of L holds a [= Top L let a be Element of L; ::_thesis: a [= Top L (Top L) "/\" a [= Top L by Th6; hence a [= Top L ; ::_thesis: verum end; definition let L be non empty LattStr ; let x be Element of L; assume A1: L is complemented D_Lattice ; funcx ` -> Element of L means :Def21: :: LATTICES:def 21 it is_a_complement_of x; existence ex b1 being Element of L st b1 is_a_complement_of x by A1, Def19; uniqueness for b1, b2 being Element of L st b1 is_a_complement_of x & b2 is_a_complement_of x holds b1 = b2 proof let a, b be Element of L; ::_thesis: ( a is_a_complement_of x & b is_a_complement_of x implies a = b ) assume that A2: a is_a_complement_of x and A3: b is_a_complement_of x ; ::_thesis: a = b A4: ( x "\/" b = Top L & x "/\" b = Bottom L ) by A3, Def18; ( x "\/" a = Top L & x "/\" a = Bottom L ) by A2, Def18; hence a = b by A1, A4, Th12; ::_thesis: verum end; end; :: deftheorem Def21 defines ` LATTICES:def_21_:_ for L being non empty LattStr for x being Element of L st L is complemented D_Lattice holds for b3 being Element of L holds ( b3 = x ` iff b3 is_a_complement_of x ); theorem Th20: :: LATTICES:20 for L being B_Lattice for a being Element of L holds (a `) "/\" a = Bottom L proof let L be B_Lattice; ::_thesis: for a being Element of L holds (a `) "/\" a = Bottom L let a be Element of L; ::_thesis: (a `) "/\" a = Bottom L a ` is_a_complement_of a by Def21; hence (a `) "/\" a = Bottom L by Def18; ::_thesis: verum end; theorem Th21: :: LATTICES:21 for L being B_Lattice for a being Element of L holds (a `) "\/" a = Top L proof let L be B_Lattice; ::_thesis: for a being Element of L holds (a `) "\/" a = Top L let a be Element of L; ::_thesis: (a `) "\/" a = Top L a ` is_a_complement_of a by Def21; hence (a `) "\/" a = Top L by Def18; ::_thesis: verum end; registration let L be B_Lattice; let a be Element of L; reduce(a `) ` to a; reducibility (a `) ` = a proof a ` is_a_complement_of a by Def21; then A1: ( a "\/" (a `) = Top L & a "/\" (a `) = Bottom L ) by Def18; (a `) ` is_a_complement_of a ` by Def21; then ( ((a `) `) "\/" (a `) = Top L & ((a `) `) "/\" (a `) = Bottom L ) by Def18; hence (a `) ` = a by A1, Th12; ::_thesis: verum end; end; theorem :: LATTICES:22 for L being B_Lattice for a being Element of L holds (a `) ` = a ; theorem Th23: :: LATTICES:23 for L being B_Lattice for a, b being Element of L holds (a "/\" b) ` = (a `) "\/" (b `) proof let L be B_Lattice; ::_thesis: for a, b being Element of L holds (a "/\" b) ` = (a `) "\/" (b `) let a, b be Element of L; ::_thesis: (a "/\" b) ` = (a `) "\/" (b `) A1: ((a `) "\/" (b `)) "/\" (a "/\" b) = (((a `) "\/" (b `)) "/\" a) "/\" b by Def7 .= (((a `) "/\" a) "\/" ((b `) "/\" a)) "/\" b by Def11 .= ((Bottom L) "\/" ((b `) "/\" a)) "/\" b by Th20 .= (b "/\" (b `)) "/\" a by Def7 .= (Bottom L) "/\" a by Th20 .= Bottom L ; ((a `) "\/" (b `)) "\/" (a "/\" b) = (a `) "\/" ((b `) "\/" (a "/\" b)) by Def5 .= (a `) "\/" (((b `) "\/" a) "/\" ((b `) "\/" b)) by Th11 .= (a `) "\/" (((b `) "\/" a) "/\" (Top L)) by Th21 .= (b `) "\/" (a "\/" (a `)) by Def5 .= (b `) "\/" (Top L) by Th21 .= Top L ; then (a `) "\/" (b `) is_a_complement_of a "/\" b by A1, Def18; hence (a "/\" b) ` = (a `) "\/" (b `) by Def21; ::_thesis: verum end; theorem :: LATTICES:24 for L being B_Lattice for a, b being Element of L holds (a "\/" b) ` = (a `) "/\" (b `) proof let L be B_Lattice; ::_thesis: for a, b being Element of L holds (a "\/" b) ` = (a `) "/\" (b `) let a, b be Element of L; ::_thesis: (a "\/" b) ` = (a `) "/\" (b `) thus (a "\/" b) ` = (((a `) `) "\/" ((b `) `)) ` .= (((a `) "/\" (b `)) `) ` by Th23 .= (a `) "/\" (b `) ; ::_thesis: verum end; theorem Th25: :: LATTICES:25 for L being B_Lattice for b, a being Element of L holds ( b "/\" a = Bottom L iff b [= a ` ) proof let L be B_Lattice; ::_thesis: for b, a being Element of L holds ( b "/\" a = Bottom L iff b [= a ` ) let b, a be Element of L; ::_thesis: ( b "/\" a = Bottom L iff b [= a ` ) thus ( b "/\" a = Bottom L implies b [= a ` ) ::_thesis: ( b [= a ` implies b "/\" a = Bottom L ) proof assume A1: b "/\" a = Bottom L ; ::_thesis: b [= a ` b = b "/\" (Top L) .= b "/\" (a "\/" (a `)) by Th21 .= (Bottom L) "\/" (b "/\" (a `)) by A1, Def11 .= b "/\" (a `) ; then b "\/" (a `) = a ` by Def8; hence b [= a ` by Def3; ::_thesis: verum end; thus ( b [= a ` implies b "/\" a = Bottom L ) ::_thesis: verum proof assume b [= a ` ; ::_thesis: b "/\" a = Bottom L then b "/\" a [= (a `) "/\" a by Th9; then A2: b "/\" a [= Bottom L by Th20; Bottom L [= b "/\" a by Th16; hence b "/\" a = Bottom L by A2, Th8; ::_thesis: verum end; end; theorem :: LATTICES:26 for L being B_Lattice for a, b being Element of L st a [= b holds b ` [= a ` proof let L be B_Lattice; ::_thesis: for a, b being Element of L st a [= b holds b ` [= a ` let a, b be Element of L; ::_thesis: ( a [= b implies b ` [= a ` ) assume a [= b ; ::_thesis: b ` [= a ` then (b `) "/\" a [= (b `) "/\" b by Th9; then A1: (b `) "/\" a [= Bottom L by Th20; Bottom L [= (b `) "/\" a by Th16; then (b `) "/\" a = Bottom L by A1, Th8; hence b ` [= a ` by Th25; ::_thesis: verum end; begin definition let L be Lattice; let S be Subset of L; attrS is initial means :Def22: :: LATTICES:def 22 for p, q being Element of L st p [= q & q in S holds p in S; attrS is final means :Def23: :: LATTICES:def 23 for p, q being Element of L st p [= q & p in S holds q in S; attrS is meet-closed means :: LATTICES:def 24 for p, q being Element of L st p in S & q in S holds p "/\" q in S; attrS is join-closed means :: LATTICES:def 25 for p, q being Element of L st p in S & q in S holds p "\/" q in S; end; :: deftheorem Def22 defines initial LATTICES:def_22_:_ for L being Lattice for S being Subset of L holds ( S is initial iff for p, q being Element of L st p [= q & q in S holds p in S ); :: deftheorem Def23 defines final LATTICES:def_23_:_ for L being Lattice for S being Subset of L holds ( S is final iff for p, q being Element of L st p [= q & p in S holds q in S ); :: deftheorem defines meet-closed LATTICES:def_24_:_ for L being Lattice for S being Subset of L holds ( S is meet-closed iff for p, q being Element of L st p in S & q in S holds p "/\" q in S ); :: deftheorem defines join-closed LATTICES:def_25_:_ for L being Lattice for S being Subset of L holds ( S is join-closed iff for p, q being Element of L st p in S & q in S holds p "\/" q in S ); registration let L be Lattice; cluster [#] L -> non empty initial final ; coherence ( [#] L is initial & [#] L is final & not [#] L is empty ) proof thus [#] L is initial ::_thesis: ( [#] L is final & not [#] L is empty ) proof let p, q be Element of L; :: according to LATTICES:def_22 ::_thesis: ( p [= q & q in [#] L implies p in [#] L ) thus ( p [= q & q in [#] L implies p in [#] L ) ; ::_thesis: verum end; thus [#] L is final ::_thesis: not [#] L is empty proof let p, q be Element of L; :: according to LATTICES:def_23 ::_thesis: ( p [= q & p in [#] L implies q in [#] L ) thus ( p [= q & p in [#] L implies q in [#] L ) ; ::_thesis: verum end; thus not [#] L is empty ; ::_thesis: verum end; end; registration let L be Lattice; cluster non empty initial final for M2( bool the carrier of L); existence ex b1 being Subset of L st ( b1 is initial & b1 is final & not b1 is empty ) proof take [#] L ; ::_thesis: ( [#] L is initial & [#] L is final & not [#] L is empty ) thus ( [#] L is initial & [#] L is final & not [#] L is empty ) ; ::_thesis: verum end; cluster empty -> initial final for M2( bool the carrier of L); coherence for b1 being Subset of L st b1 is empty holds ( b1 is initial & b1 is final ) proof let S be Subset of L; ::_thesis: ( S is empty implies ( S is initial & S is final ) ) assume A1: S is empty ; ::_thesis: ( S is initial & S is final ) thus S is initial ::_thesis: S is final proof let p be Element of L; :: according to LATTICES:def_22 ::_thesis: for q being Element of L st p [= q & q in S holds p in S thus for q being Element of L st p [= q & q in S holds p in S by A1; ::_thesis: verum end; let p be Element of L; :: according to LATTICES:def_23 ::_thesis: for q being Element of L st p [= q & p in S holds q in S thus for q being Element of L st p [= q & p in S holds q in S by A1; ::_thesis: verum end; cluster initial -> meet-closed for M2( bool the carrier of L); coherence for b1 being Subset of L st b1 is initial holds b1 is meet-closed proof let S be Subset of L; ::_thesis: ( S is initial implies S is meet-closed ) assume A2: S is initial ; ::_thesis: S is meet-closed let p, q be Element of L; :: according to LATTICES:def_24 ::_thesis: ( p in S & q in S implies p "/\" q in S ) assume that p in S and A3: q in S ; ::_thesis: p "/\" q in S thus p "/\" q in S by A2, A3, Def22, Th6; ::_thesis: verum end; cluster final -> join-closed for M2( bool the carrier of L); coherence for b1 being Subset of L st b1 is final holds b1 is join-closed proof let S be Subset of L; ::_thesis: ( S is final implies S is join-closed ) assume A4: S is final ; ::_thesis: S is join-closed let p, q be Element of L; :: according to LATTICES:def_25 ::_thesis: ( p in S & q in S implies p "\/" q in S ) assume that p in S and A5: q in S ; ::_thesis: p "\/" q in S thus p "\/" q in S by A4, A5, Def23, Th5; ::_thesis: verum end; end; theorem :: LATTICES:27 for L being Lattice for S being non empty initial final Subset of L holds S = [#] L proof let L be Lattice; ::_thesis: for S being non empty initial final Subset of L holds S = [#] L let S be non empty initial final Subset of L; ::_thesis: S = [#] 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; ::_thesis: ( x in S iff x in [#] L ) thus ( x in S implies x in [#] L ) ; ::_thesis: ( x in [#] L implies x in S ) assume x in [#] L ; ::_thesis: x in S A2: x "/\" p in S by A1, Def22, Th6; thus x in S by A2, Def23, Th6; ::_thesis: verum end; hence S = [#] L by SUBSET_1:3; ::_thesis: verum end;