:: A Characterization of Concept Lattices; Dual Concept Lattices :: by Christoph Schwarzweller :: :: Received August 17, 1999 :: Copyright (c) 1999-2012 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 CONLAT_1, STRUCT_0, QC_LANG1, SUBSET_1, LATTICES, XXREAL_2, PBOOLE, EQREL_1, XBOOLE_0, SETFAM_1, FUNCT_1, TARSKI, CAT_1, LATTICE3, ZFMISC_1, RELAT_1, FUNCT_3, LATTICE6, REWRITE1, GROUP_6, WELLORD1, FUNCT_2, MCART_1, FILTER_1, XXREAL_0, ORDERS_2, CONLAT_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, XTUPLE_0, MCART_1, FUNCT_1, DOMAIN_1, RELSET_1, ORDERS_2, STRUCT_0, LATTICE2, LATTICE3, LATTICE6, PARTFUN1, FUNCT_2, LATTICES, LATTICE4, CONLAT_1; constructors DOMAIN_1, LATTICE2, LATTICE4, CONLAT_1, LATTICE6, RELSET_1, XTUPLE_0; registrations SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES, LATTICE2, LATTICE3, CONLAT_1, RELSET_1, XTUPLE_0; requirements SUBSET, BOOLE; definitions TARSKI, LATTICE3, VECTSP_8, LATTICE6, FUNCT_1, XBOOLE_0, SUBSET_1, XTUPLE_0; theorems TARSKI, RELAT_1, FUNCT_1, ZFMISC_1, LATTICE4, LATTICES, LATTICE3, LATTICE6, MCART_1, SETFAM_1, FUNCT_2, FILTER_1, LATTICE2, ORDERS_2, CONLAT_1, XBOOLE_0, XTUPLE_0; schemes FUNCT_2; begin definition let C be FormalContext; let CP be strict FormalConcept of C; func @CP -> Element of ConceptLattice(C) equals CP; coherence proof ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by CONLAT_1:def 20; hence thesis by CONLAT_1:31; end; end; registration let C be FormalContext; cluster ConceptLattice C -> bounded; coherence proof A1: (@Concept-with-all-Objects(C))@ = Concept-with-all-Objects(C) by CONLAT_1:def 21; A2: for a being Element of ConceptLattice(C) holds a [= @ Concept-with-all-Objects(C) proof let a be Element of ConceptLattice(C); a@ is-SubConcept-of (@Concept-with-all-Objects(C))@ by A1,CONLAT_1:30; hence thesis by CONLAT_1:43; end; for a being Element of ConceptLattice(C) holds @ Concept-with-all-Objects(C) "\/" a = @Concept-with-all-Objects(C) & a "\/" @ Concept-with-all-Objects(C) = @Concept-with-all-Objects(C) proof let a be Element of ConceptLattice(C); a [= @Concept-with-all-Objects(C) by A2; hence thesis by LATTICES:def 3; end; then A3: ConceptLattice C is upper-bounded by LATTICES:def 14; A4: (@Concept-with-all-Attributes(C))@ = Concept-with-all-Attributes(C) by CONLAT_1:def 21; A5: for a being Element of ConceptLattice(C) holds @ Concept-with-all-Attributes(C) [= a proof let a be Element of ConceptLattice(C); (@Concept-with-all-Attributes(C))@ is-SubConcept-of a@ by A4,CONLAT_1:30; hence thesis by CONLAT_1:43; end; for a being Element of ConceptLattice(C) holds @ Concept-with-all-Attributes(C) "/\" a = @Concept-with-all-Attributes(C) & a "/\" @Concept-with-all-Attributes(C) = @Concept-with-all-Attributes(C) proof let a be Element of ConceptLattice(C); @Concept-with-all-Attributes(C) [= a by A5; hence thesis by LATTICES:4; end; then ConceptLattice C is lower-bounded by LATTICES:def 13; hence thesis by A3; end; end; theorem Th1: for C being FormalContext holds Bottom (ConceptLattice(C)) = Concept-with-all-Attributes(C) & Top (ConceptLattice(C)) = Concept-with-all-Objects(C) proof let C be FormalContext; A1: (@Concept-with-all-Objects(C))@ = Concept-with-all-Objects(C) by CONLAT_1:def 21; A2: for a being Element of ConceptLattice(C) holds a [= @ Concept-with-all-Objects(C) proof let a be Element of ConceptLattice(C); a@ is-SubConcept-of (@Concept-with-all-Objects(C))@ by A1,CONLAT_1:30; hence thesis by CONLAT_1:43; end; A3: for a being Element of ConceptLattice(C) holds @Concept-with-all-Objects (C) "\/" a = @Concept-with-all-Objects(C) & a "\/" @Concept-with-all-Objects(C) = @Concept-with-all-Objects(C) proof let a be Element of ConceptLattice(C); a [= @Concept-with-all-Objects(C) by A2; hence thesis by LATTICES:def 3; end; A4: (@Concept-with-all-Attributes(C))@ = Concept-with-all-Attributes(C) by CONLAT_1:def 21; A5: for a being Element of ConceptLattice(C) holds @ Concept-with-all-Attributes(C) [= a proof let a be Element of ConceptLattice(C); (@Concept-with-all-Attributes(C))@ is-SubConcept-of a@ by A4,CONLAT_1:30; hence thesis by CONLAT_1:43; end; for a being Element of ConceptLattice(C) holds @ Concept-with-all-Attributes(C) "/\" a = @Concept-with-all-Attributes(C) & a "/\" @Concept-with-all-Attributes(C) = @Concept-with-all-Attributes(C) proof let a be Element of ConceptLattice(C); @Concept-with-all-Attributes(C) [= a by A5; hence thesis by LATTICES:4; end; hence thesis by A3,LATTICES:def 16,def 17; end; theorem Th2: for C being FormalContext for D being non empty Subset-Family of the carrier of C holds (ObjectDerivation(C)).(union D) = meet({( ObjectDerivation(C)).O where O is Subset of the carrier of C : O in D}) proof let C be FormalContext; let D be non empty Subset-Family of(the carrier of C); reconsider D9=D as non empty Subset-Family of the carrier of C; set OU = (ObjectDerivation(C)).(union D); set M = meet({(ObjectDerivation(C)).O where O is Subset of the carrier of C : O in D}); per cases; suppose A1: {(ObjectDerivation(C)).O where O is Subset of the carrier of C : O in D} <> {}; thus OU c= M proof let x be set; assume x in OU; then x in {a9 where a9 is Attribute of C : for o being Object of C st o in union D9 holds o is-connected-with a9} by CONLAT_1:def 3; then A2: ex x9 being Attribute of C st x9 = x & for o being Object of C st o in union D holds o is-connected-with x9; then reconsider x as Attribute of C; A3: for O being Subset of the carrier of C st O in D for o being Object of C st o in O holds o is-connected-with x proof let O be Subset of the carrier of C; assume A4: O in D; let o be Object of C; assume o in O; then o in union D by A4,TARSKI:def 4; hence thesis by A2; end; A5: for O being Subset of the carrier of C st O in D holds x in ( ObjectDerivation(C)).O proof let O be Subset of the carrier of C; assume O in D; then for o being Object of C st o in O holds o is-connected-with x by A3; then x in {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a }; hence thesis by CONLAT_1:def 3; end; for Y being set holds Y in {(ObjectDerivation(C)).O where O is Subset of the carrier of C : O in D} implies x in Y proof let Y be set; assume Y in {(ObjectDerivation(C)).O where O is Subset of the carrier of C : O in D}; then ex O being Subset of the carrier of C st Y = ( ObjectDerivation(C) ).O & O in D; hence thesis by A5; end; hence thesis by A1,SETFAM_1:def 1; end; thus M c= OU proof set d = the Element of {(ObjectDerivation(C)).O where O is Subset of the carrier of C : O in D}; let x be set; assume A6: x in M; then A7: x in d by A1,SETFAM_1:def 1; d in {(ObjectDerivation(C)).O where O is Subset of the carrier of C : O in D} by A1; then ex X being Subset of the carrier of C st d = ( ObjectDerivation(C)). X & X in D; then reconsider x as Attribute of C by A7; A8: for O being Subset of the carrier of C st O in D holds x in ( ObjectDerivation(C)).O proof let O be Subset of the carrier of C; assume O in D; then (ObjectDerivation(C)).O in {(ObjectDerivation(C)).O9 where O9 is Subset of the carrier of C : O9 in D}; hence thesis by A6,SETFAM_1:def 1; end; A9: for O being Subset of the carrier of C st O in D for o being Object of C st o in O holds o is-connected-with x proof let O be Subset of the carrier of C; assume O in D; then x in (ObjectDerivation(C)).O by A8; then x in {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a} by CONLAT_1:def 3; then A10: ex x9 being Attribute of C st x9 = x & for o being Object of C st o in O holds o is-connected-with x9; let o be Object of C; assume o in O; hence thesis by A10; end; for o being Object of C st o in union D holds o is-connected-with x proof let o be Object of C; assume o in union D; then ex Y being set st o in Y & Y in D by TARSKI:def 4; hence thesis by A9; end; then x in {a9 where a9 is Attribute of C : for o being Object of C st o in union D9 holds o is-connected-with a9}; hence thesis by CONLAT_1:def 3; end; end; suppose A11: {(ObjectDerivation(C)).O where O is Subset of the carrier of C : O in D} = {}; D = {} proof set x = the Element of D; assume D <> {}; (ObjectDerivation(C)).x in {(ObjectDerivation(C)).O where O is Subset of the carrier of C : O in D}; hence thesis by A11; end; hence thesis; end; end; theorem Th3: for C being FormalContext for D being non empty Subset-Family of( the carrier' of C) holds (AttributeDerivation(C)).(union D) = meet({( AttributeDerivation(C)).A where A is Subset of the carrier' of C : A in D}) proof let C be FormalContext; let D be non empty Subset-Family of(the carrier' of C); reconsider D9=D as non empty Subset-Family of the carrier' of C; set OU = (AttributeDerivation(C)).(union D); set M = meet({(AttributeDerivation(C)).A where A is Subset of the carrier' of C : A in D}); now per cases; case A1: {(AttributeDerivation(C)).A where A is Subset of the carrier' of C: A in D} <> {}; thus OU = M proof thus OU c= M proof let x be set; assume x in OU; then x in {o9 where o9 is Object of C : for a being Attribute of C st a in union D9 holds o9 is-connected-with a} by CONLAT_1:def 4; then A2: ex x9 being Object of C st x9 = x & for a being Attribute of C st a in union D holds x9 is-connected-with a; then reconsider x as Object of C; A3: for A being Subset of the carrier' of C st A in D for a being Attribute of C st a in A holds x is-connected-with a proof let A be Subset of the carrier' of C; assume A4: A in D; let a be Attribute of C; assume a in A; then a in union D by A4,TARSKI:def 4; hence thesis by A2; end; A5: for A being Subset of the carrier' of C st A in D holds x in ( AttributeDerivation(C)).A proof let A be Subset of the carrier' of C; assume A in D; then for a being Attribute of C st a in A holds x is-connected-with a by A3; then x in {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}; hence thesis by CONLAT_1:def 4; end; for Y being set holds Y in {(AttributeDerivation(C)).A where A is Subset of the carrier' of C : A in D} implies x in Y proof let Y be set; assume Y in {(AttributeDerivation(C)).A where A is Subset of the carrier' of C : A in D}; then ex A being Subset of the carrier' of C st Y = ( AttributeDerivation(C)).A & A in D; hence thesis by A5; end; hence thesis by A1,SETFAM_1:def 1; end; set d = the Element of {(AttributeDerivation(C)).A where A is Subset of the carrier' of C : A in D}; let x be set; assume A6: x in M; then A7: x in d by A1,SETFAM_1:def 1; d in {(AttributeDerivation(C)).A where A is Subset of the carrier' of C : A in D} by A1; then ex X being Subset of the carrier' of C st d = ( AttributeDerivation(C)).X & X in D; then reconsider x as Object of C by A7; A8: for A being Subset of the carrier' of C st A in D holds x in ( AttributeDerivation(C)).A proof let A be Subset of the carrier' of C; assume A in D; then (AttributeDerivation(C)).A in {(AttributeDerivation(C)).A9 where A9 is Subset of the carrier' of C : A9 in D}; hence thesis by A6,SETFAM_1:def 1; end; A9: for A being Subset of the carrier' of C st A in D for a being Attribute of C st a in A holds x is-connected-with a proof let A be Subset of the carrier' of C; assume A in D; then x in (AttributeDerivation(C)).A by A8; then x in {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a} by CONLAT_1:def 4; then A10: ex x9 being Object of C st x9 = x & for a being Attribute of C st a in A holds x9 is-connected-with a; let a be Attribute of C; assume a in A; hence thesis by A10; end; for a being Attribute of C st a in union D holds x is-connected-with a proof let a be Attribute of C; assume a in union D; then ex Y being set st a in Y & Y in D by TARSKI:def 4; hence thesis by A9; end; then x in {o9 where o9 is Object of C : for a being Attribute of C st a in union D9 holds o9 is-connected-with a}; hence thesis by CONLAT_1:def 4; end; end; case A11: {(AttributeDerivation(C)).A where A is Subset of the carrier' of C : A in D} = {}; D = {} proof set x = the Element of D; assume D <> {}; (AttributeDerivation(C)).x in {(AttributeDerivation(C)).A where A is Subset of the carrier' of C : A in D}; hence thesis by A11; end; hence thesis; end; end; hence thesis; end; theorem Th4: for C being FormalContext for D being Subset of ConceptLattice(C) holds "/\"(D,ConceptLattice(C)) is FormalConcept of C & "\/"(D,ConceptLattice(C )) is FormalConcept of C proof let C be FormalContext; let D be Subset of ConceptLattice(C); ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by CONLAT_1:def 20; hence thesis by CONLAT_1:31; end; definition let C be FormalContext; let D be Subset of ConceptLattice(C); func "/\"(D,C) -> FormalConcept of C equals "/\"(D,ConceptLattice(C)); coherence by Th4; func "\/"(D,C) -> FormalConcept of C equals "\/"(D,ConceptLattice(C)); coherence by Th4; end; theorem for C being FormalContext holds "\/"({} ConceptLattice(C),C) = Concept-with-all-Attributes(C) & "/\"({} ConceptLattice(C),C) = Concept-with-all-Objects(C) proof let C be FormalContext; A1: for b being Element of ConceptLattice(C) st b is_less_than {} holds b [= @Concept-with-all-Objects(C) proof let b be Element of ConceptLattice(C); assume b is_less_than {}; b@ is-SubConcept-of Concept-with-all-Objects(C) & Concept-with-all-Objects(C ) = (@Concept-with-all-Objects(C))@ by CONLAT_1:30 ,def 21; hence thesis by CONLAT_1:43; end; for q being Element of ConceptLattice(C) st q in {} holds @ Concept-with-all-Objects(C) [= q; then "\/"({} ConceptLattice(C),C) = Bottom ConceptLattice(C) & @ Concept-with-all-Objects(C) is_less_than {} by LATTICE3:49,def 16; hence thesis by A1,Th1,LATTICE3:34; end; theorem for C being FormalContext holds "\/"([#] the carrier of ConceptLattice (C),C) = Concept-with-all-Objects(C) & "/\"([#] the carrier of ConceptLattice(C ),C) = Concept-with-all-Attributes(C) proof let C be FormalContext; A1: @Concept-with-all-Attributes(C) is_less_than [#] the carrier of ConceptLattice(C) proof let q be Element of ConceptLattice(C); assume q in [#] the carrier of ConceptLattice(C); Concept-with-all-Attributes(C) is-SubConcept-of q@ & Concept-with-all-Attributes(C) = (@Concept-with-all-Attributes(C))@ by CONLAT_1:30,def 21; hence thesis by CONLAT_1:43; end; "\/"(the carrier of ConceptLattice(C),ConceptLattice(C)) = Top ConceptLattice (C) & for b being Element of ConceptLattice(C) st b is_less_than [#] the carrier of ConceptLattice(C) holds b [= @Concept-with-all-Attributes(C) by LATTICE3:50,def 16; hence thesis by A1,Th1,LATTICE3:34; end; theorem for C being FormalContext for D being non empty Subset of ConceptLattice(C) holds the Extent of "\/"(D,C) = (AttributeDerivation(C)).(( ObjectDerivation(C)). union {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} ) & the Intent of "\/"(D,C) = meet {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D} proof let C be FormalContext; let D be non empty Subset of ConceptLattice(C); set O = (AttributeDerivation(C)).((ObjectDerivation(C)). union {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}); set A9 = (ObjectDerivation(C)). union {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr (#E,I#) in D}; set y = the Element of D; {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} c= bool (the carrier of C) proof let x be set; assume x in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; then ex E being Subset of the carrier of C, I being Subset of the carrier' of C st x = the Extent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D; hence thesis; end; then reconsider OO = {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} as Subset-Family of (the carrier of C); O c= the carrier of C proof set u = union {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; u c= the carrier of C proof let x be set; assume x in u; then consider Y being set such that A1: x in Y and A2: Y in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} by TARSKI:def 4; ex E being Subset of the carrier of C, I being Subset of the carrier' of C st Y = the Extent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D by A2; hence thesis by A1; end; then reconsider u as Subset of the carrier of C; let x be set; A3: (AttributeDerivation(C)).((ObjectDerivation(C)).u) is Element of bool (the carrier of C); assume x in O; hence thesis by A3; end; then reconsider o = O as Subset of the carrier of C; A4: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by CONLAT_1:def 20; A5: for x being set holds x in D implies x is strict FormalConcept of C & ex E being Subset of the carrier of C, I being Subset of the carrier' of C st x = ConceptStr(#E,I#) proof let x be set; assume x in D; then x is strict FormalConcept of C by A4,CONLAT_1:31; hence thesis; end; then ex E9 being Subset of the carrier of C, I9 being Subset of the carrier' of C st y = ConceptStr(#E9,I9#); then the Extent of y in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; then reconsider OO as non empty Subset-Family of (the carrier of C); A6: {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} c= {( ObjectDerivation(C)).O9 where O9 is Subset of the carrier of C : O9 in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}} proof let x be set; assume x in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; then consider E being Subset of the carrier of C, I being Subset of the carrier' of C such that A7: x = the Intent of ConceptStr(#E,I#) and A8: ConceptStr(#E,I#) in D; ConceptStr(#E,I#) is FormalConcept of C by A5,A8; then A9: x = (ObjectDerivation(C)).(the Extent of ConceptStr(#E,I#)) by A7, CONLAT_1:def 10; the Extent of ConceptStr(#E,I#) in {the Extent of ConceptStr(#EE,II #) where EE is Subset of the carrier of C, II is Subset of the carrier' of C : ConceptStr(#EE,II#) in D} by A8; hence thesis by A9; end; {(ObjectDerivation(C)).O9 where O9 is Subset of the carrier of C : O9 in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}} c= {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} proof let x be set; assume x in {(ObjectDerivation(C)).O9 where O9 is Subset of the carrier of C : O9 in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}}; then consider O9 being Subset of the carrier of C such that A10: x = (ObjectDerivation(C)).O9 and A11: O9 in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; consider E being Subset of the carrier of C, I being Subset of the carrier' of C such that A12: O9 = the Extent of ConceptStr(#E,I#) and A13: ConceptStr(#E,I#) in D by A11; ConceptStr(#E,I#) is FormalConcept of C by A5,A13; then x = the Intent of ConceptStr(#E,I#) by A10,A12,CONLAT_1:def 10; hence thesis by A13; end; then A14: {(ObjectDerivation(C)).O9 where O9 is Subset of the carrier of C : O9 in { the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}} = {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} by A6,XBOOLE_0:def 10; A15: A9 = meet({(ObjectDerivation(C)).O9 where O9 is Subset of the carrier of C : O9 in OO}) by Th2; A9 c= the carrier' of C proof set y = the Element of D; set Y = the Element of {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D}; let x be set; ex E9 being Subset of the carrier of C, I9 being Subset of the carrier' of C st y = ConceptStr(#E9,I9#) by A5; then A16: the Intent of y in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} ; then Y in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; then A17: ex E1 being Subset of the carrier of C, I1 being Subset of the carrier' of C st Y = the Intent of ConceptStr(#E1,I1#) & ConceptStr(#E1, I1#) in D; assume x in A9; then x in Y by A15,A14,A16,SETFAM_1:def 1; hence thesis by A17; end; then reconsider a = A9 as Subset of the carrier' of C; union {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} c= the carrier of C proof let x be set; assume x in union {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; then consider Y being set such that A18: x in Y and A19: Y in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C,I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} by TARSKI:def 4; ex E being Subset of the carrier of C, I being Subset of the carrier' of C st Y = the Extent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D by A19; hence thesis by A18; end; then reconsider CP9 = ConceptStr(#o,a#) as strict FormalConcept of C by CONLAT_1:19; reconsider CP = CP9 as Element of ConceptLattice(C) by A4,CONLAT_1:31; A20: the Intent of CP@ = meet {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D} by A15,A14,CONLAT_1:def 21; A21: for r being Element of ConceptLattice(C) st D is_less_than r holds CP [= r proof let r be Element of ConceptLattice(C); assume A22: D is_less_than r; A23: for q being Element of ConceptLattice(C) st q in D holds the Intent of r@ c= the Intent of q@ proof let q be Element of ConceptLattice(C); assume q in D; then q [= r by A22,LATTICE3:def 17; then q@ is-SubConcept-of r@ by CONLAT_1:43; hence thesis by CONLAT_1:28; end; the Intent of r@ c= meet {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D} proof set y = the Element of D; let x be set; assume A24: x in the Intent of r@; A25: for Y being set holds Y in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E ,I#) in D} implies x in Y proof let Y be set; assume Y in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; then consider Ey being Subset of the carrier of C, Iy being Subset of the carrier' of C such that A26: Y = the Intent of ConceptStr(#Ey,Iy#) and A27: ConceptStr(#Ey,Iy#) in D; reconsider C1 = ConceptStr(#Ey,Iy#) as Element of ConceptLattice(C) by A27; the Intent of r@ c= the Intent of C1@ by A23,A27; then x in the Intent of C1@ by A24; hence thesis by A26,CONLAT_1:def 21; end; ex E9 being Subset of the carrier of C, I9 being Subset of the carrier' of C st y = ConceptStr(#E9,I9#) by A5; then the Intent of y in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D}; hence thesis by A25,SETFAM_1:def 1; end; then CP@ is-SubConcept-of r@ by A20,CONLAT_1:28; hence thesis by CONLAT_1:43; end; D is_less_than CP proof let q be Element of ConceptLattice(C); assume q in D; then q@ in D by CONLAT_1:def 21; then the Intent of q@ in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D}; then the Intent of CP@ c= the Intent of q@ by A20,SETFAM_1:3; then q@ is-SubConcept-of CP@ by CONLAT_1:28; hence thesis by CONLAT_1:43; end; hence thesis by A15,A14,A21,LATTICE3:def 21; end; theorem for C being FormalContext for D being non empty Subset of ConceptLattice(C) holds the Extent of "/\"(D,C) = meet {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} & the Intent of "/\"(D,C) = ( ObjectDerivation(C)).((AttributeDerivation(C)). union {the Intent of ConceptStr (#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}) proof let C be FormalContext; let D be non empty Subset of ConceptLattice(C); set A = (ObjectDerivation(C)).((AttributeDerivation(C)). union {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}); set O9 = (AttributeDerivation(C)). union {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; set y = the Element of D; {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} c= bool (the carrier' of C) proof let x be set; assume x in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; then ex E being Subset of the carrier of C, I being Subset of the carrier' of C st x = the Intent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D; hence thesis; end; then reconsider AA = {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} as Subset-Family of (the carrier' of C); A c= the carrier' of C proof set u = union {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; u c= the carrier' of C proof let x be set; assume x in u; then consider Y being set such that A1: x in Y and A2: Y in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} by TARSKI:def 4; ex E being Subset of the carrier of C, I being Subset of the carrier' of C st Y = the Intent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D by A2; hence thesis by A1; end; then reconsider u as Subset of the carrier' of C; let x be set; A3: (ObjectDerivation(C)).((AttributeDerivation(C)).u) is Element of bool (the carrier' of C); assume x in A; hence thesis by A3; end; then reconsider a = A as Subset of the carrier' of C; A4: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by CONLAT_1:def 20; A5: for x being set holds x in D implies x is strict FormalConcept of C & ex E being Subset of the carrier of C, I being Subset of the carrier' of C st x = ConceptStr(#E,I#) proof let x be set; assume x in D; then x is strict FormalConcept of C by A4,CONLAT_1:31; hence thesis; end; then ex E9 being Subset of the carrier of C, I9 being Subset of the carrier' of C st y = ConceptStr(#E9,I9#); then the Intent of y in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; then reconsider AA as non empty Subset-Family of (the carrier' of C); A6: {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} c= {( AttributeDerivation(C)).A9 where A9 is Subset of the carrier' of C : A9 in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}} proof let x be set; assume x in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; then consider E being Subset of the carrier of C, I being Subset of the carrier' of C such that A7: x = the Extent of ConceptStr(#E,I#) and A8: ConceptStr(#E,I#) in D; ConceptStr(#E,I#) is FormalConcept of C by A5,A8; then A9: x = (AttributeDerivation(C)).(the Intent of ConceptStr(#E,I#)) by A7, CONLAT_1:def 10; the Intent of ConceptStr(#E,I#) in {the Intent of ConceptStr(#EE,II#) where EE is Subset of the carrier of C, II is Subset of the carrier' of C : ConceptStr(#EE,II#) in D} by A8; hence thesis by A9; end; {(AttributeDerivation(C)).A9 where A9 is Subset of the carrier' of C : A9 in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}} c= {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} proof let x be set; assume x in {(AttributeDerivation(C)).A9 where A9 is Subset of the carrier' of C : A9 in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}}; then consider A9 being Subset of the carrier' of C such that A10: x = (AttributeDerivation(C)).A9 and A11: A9 in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; consider E being Subset of the carrier of C, I being Subset of the carrier' of C such that A12: A9 = the Intent of ConceptStr(#E,I#) and A13: ConceptStr(#E,I#) in D by A11; ConceptStr(#E,I#) is FormalConcept of C by A5,A13; then x = the Extent of ConceptStr(#E,I#) by A10,A12,CONLAT_1:def 10; hence thesis by A13; end; then A14: {(AttributeDerivation(C)).A9 where A9 is Subset of the carrier' of C : A9 in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}} = {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} by A6,XBOOLE_0:def 10; A15: O9 = meet({(AttributeDerivation(C)).A9 where A9 is Subset of the carrier' of C : A9 in AA}) by Th3; O9 c= the carrier of C proof set y = the Element of D; set Y = the Element of {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D}; let x be set; ex E9 being Subset of the carrier of C, I9 being Subset of the carrier' of C st y = ConceptStr(#E9,I9#) by A5; then A16: the Extent of y in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} ; then Y in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; then A17: ex E1 being Subset of the carrier of C, I1 being Subset of the carrier' of C st Y = the Extent of ConceptStr(#E1,I1#) & ConceptStr(#E1, I1#) in D; assume x in O9; then x in Y by A15,A14,A16,SETFAM_1:def 1; hence thesis by A17; end; then reconsider o = O9 as Subset of the carrier of C; union {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} c= the carrier' of C proof let x be set; assume x in union {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; then consider Y being set such that A18: x in Y and A19: Y in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C,I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} by TARSKI:def 4; ex E being Subset of the carrier of C, I being Subset of the carrier' of C st Y = the Intent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D by A19; hence thesis by A18; end; then reconsider CP9 = ConceptStr(#o,a#) as strict FormalConcept of C by CONLAT_1:21; reconsider CP = CP9 as Element of ConceptLattice(C) by A4,CONLAT_1:31; A20: the Extent of CP@ = meet {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D} by A15,A14,CONLAT_1:def 21; A21: for r being Element of ConceptLattice(C) st r is_less_than D holds r [= CP proof let r be Element of ConceptLattice(C); assume A22: r is_less_than D; A23: for q being Element of ConceptLattice(C) st q in D holds the Extent of r@ c= the Extent of q@ proof let q be Element of ConceptLattice(C); assume q in D; then r [= q by A22,LATTICE3:def 16; then r@ is-SubConcept-of q@ by CONLAT_1:43; hence thesis by CONLAT_1:def 16; end; the Extent of r@ c= meet {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D} proof set y = the Element of D; let x be set; assume A24: x in the Extent of r@; A25: for Y being set holds Y in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E ,I#) in D} implies x in Y proof let Y be set; assume Y in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}; then consider Ey being Subset of the carrier of C, Iy being Subset of the carrier' of C such that A26: Y = the Extent of ConceptStr(#Ey,Iy#) and A27: ConceptStr(#Ey,Iy#) in D; reconsider C1 = ConceptStr(#Ey,Iy#) as Element of ConceptLattice(C) by A27; the Extent of r@ c= the Extent of C1@ by A23,A27; then x in the Extent of C1@ by A24; hence thesis by A26,CONLAT_1:def 21; end; ex E9 being Subset of the carrier of C, I9 being Subset of the carrier' of C st y = ConceptStr(#E9,I9#) by A5; then the Extent of y in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D}; hence thesis by A25,SETFAM_1:def 1; end; then r@ is-SubConcept-of CP@ by A20,CONLAT_1:def 16; hence thesis by CONLAT_1:43; end; CP is_less_than D proof let q be Element of ConceptLattice(C); assume q in D; then q@ in D by CONLAT_1:def 21; then the Extent of q@ in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D}; then the Extent of CP@ c= the Extent of q@ by A20,SETFAM_1:3; then CP@ is-SubConcept-of q@ by CONLAT_1:def 16; hence thesis by CONLAT_1:43; end; hence thesis by A15,A14,A21,LATTICE3:34; end; theorem Th9: for C being FormalContext for CP being strict FormalConcept of C holds "\/"({ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st o in the Extent of CP & O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = ( ObjectDerivation(C)).{o}}, ConceptLattice(C)) = CP proof let C be FormalContext; let CP be strict FormalConcept of C; set D = {ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st o in the Extent of CP & O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = ( ObjectDerivation(C)).{o}}; A1: for CP9 being Element of ConceptLattice(C) st D is_less_than CP9 holds @CP [= CP9 proof let CP9 be Element of ConceptLattice(C); assume A2: D is_less_than CP9; A3: the Extent of CP c= the Extent of (CP9)@ proof let x be set; assume A4: x in the Extent of CP; then reconsider x as Element of C; set Ax = (ObjectDerivation(C)).{x}; set Ox = (AttributeDerivation(C)).((ObjectDerivation(C)).{x}); reconsider Cx = ConceptStr(#Ox,Ax#) as strict FormalConcept of C by CONLAT_1:19; Cx in {ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st o in the Extent of CP & O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = ( ObjectDerivation(C)).{o}} by A4; then @Cx [= CP9 by A2,LATTICE3:def 17; then A5: (@Cx)@ is-SubConcept-of (CP9)@ by CONLAT_1:43; {x} c= Ox by CONLAT_1:5; then A6: x in the Extent of Cx by ZFMISC_1:31; Cx = (@Cx)@ by CONLAT_1:def 21; then the Extent of Cx c= the Extent of (CP9)@ by A5,CONLAT_1:def 16; hence thesis by A6; end; CP = (@CP)@ by CONLAT_1:def 21; then (@CP)@ is-SubConcept-of (CP9)@ by A3,CONLAT_1:def 16; hence thesis by CONLAT_1:43; end; D is_less_than @CP proof let q be Element of ConceptLattice(C); assume q in D; then consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A7: q = ConceptStr(#O,A#) and A8: ex o being Object of C st o in the Extent of CP & O = ( AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (ObjectDerivation(C)) .{o}; consider o being Object of C such that A9: o in the Extent of CP and O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) and A10: A = (ObjectDerivation(C)).{o} by A8; A11: {o} c= the Extent of CP by A9,ZFMISC_1:31; (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP & the Intent of q@ = (ObjectDerivation(C)).{o} by A7,A10,CONLAT_1:def 10,def 21; then the Intent of CP c= the Intent of q@ by A11,CONLAT_1:3; then A12: q@ is-SubConcept-of CP by CONLAT_1:28; CP = (@CP)@ by CONLAT_1:def 21; hence thesis by A12,CONLAT_1:43; end; hence thesis by A1,LATTICE3:def 21; end; theorem Th10: for C being FormalContext for CP being strict FormalConcept of C holds "/\"({ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st a in the Intent of CP & O = (AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).(( AttributeDerivation(C)).{a})}, ConceptLattice(C)) = CP proof let C be FormalContext; let CP be strict FormalConcept of C; set D = {ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st a in the Intent of CP & O = (AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).(( AttributeDerivation(C)).{a})}; A1: for CP9 being Element of ConceptLattice(C) st CP9 is_less_than D holds CP9 [= @CP proof let CP9 be Element of ConceptLattice(C); assume A2: CP9 is_less_than D; A3: the Intent of CP c= the Intent of (CP9)@ proof let x be set; assume A4: x in the Intent of CP; then reconsider x as Element of the carrier' of C; set Ax = (ObjectDerivation(C)).((AttributeDerivation(C)).{x}); set Ox = (AttributeDerivation(C)).{x}; reconsider Cx = ConceptStr(#Ox,Ax#) as strict FormalConcept of C by CONLAT_1:21; Cx in {ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st a in the Intent of CP & O = (AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).(( AttributeDerivation(C)).{a}) } by A4; then CP9 [= @Cx by A2,LATTICE3:def 16; then A5: (CP9)@ is-SubConcept-of (@Cx)@ by CONLAT_1:43; {x} c= Ax by CONLAT_1:6; then A6: x in the Intent of Cx by ZFMISC_1:31; Cx = (@Cx)@ by CONLAT_1:def 21; then the Intent of Cx c= the Intent of (CP9)@ by A5,CONLAT_1:28; hence thesis by A6; end; CP = (@CP)@ by CONLAT_1:def 21; then (CP9)@ is-SubConcept-of (@CP)@ by A3,CONLAT_1:28; hence thesis by CONLAT_1:43; end; @CP is_less_than D proof let q be Element of ConceptLattice(C); assume q in D; then consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A7: q = ConceptStr(#O,A#) and A8: ex a being Attribute of C st a in the Intent of CP & O = ( AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((AttributeDerivation(C )).{a}); consider a being Attribute of C such that A9: a in the Intent of CP and A10: O = (AttributeDerivation(C)).{a} and A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by A8; A11: {a} c= the Intent of CP by A9,ZFMISC_1:31; (AttributeDerivation(C)).(the Intent of CP) = the Extent of CP & the Extent of q@ = (AttributeDerivation(C)).{a} by A7,A10,CONLAT_1:def 10,def 21; then the Extent of CP c= the Extent of q@ by A11,CONLAT_1:4; then A12: CP is-SubConcept-of q@ by CONLAT_1:def 16; CP = (@CP)@ by CONLAT_1:def 21; hence thesis by A12,CONLAT_1:43; end; hence thesis by A1,LATTICE3:34; end; definition let C be FormalContext; func gamma(C) -> Function of the carrier of C, the carrier of ConceptLattice (C) means :Def4: for o being Element of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st it.o = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (ObjectDerivation(C)).{o}; existence proof defpred P[set, set] means ex O being Subset of the carrier of C, A being Subset of the carrier' of C st $2 = ConceptStr(#O,A#) & O = ( AttributeDerivation(C)).((ObjectDerivation(C)).{$1}) & A = (ObjectDerivation(C) ).{$1}; A1: for e being set st e in the carrier of C ex u being set st u in the carrier of ConceptLattice(C) & P[e,u] proof let e be set; assume e in the carrier of C; then reconsider se = {e} as Subset of the carrier of C by ZFMISC_1:31; set A = (ObjectDerivation(C)).se; set O = (AttributeDerivation(C)).((ObjectDerivation(C)).se); take ConceptStr(#O,A#); ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) & ConceptStr (#O,A#) is FormalConcept of C by CONLAT_1:19,def 20; hence thesis by CONLAT_1:31; end; consider f being Function of the carrier of C, the carrier of ConceptLattice(C) such that A2: for e being set st e in the carrier of C holds P[e,f.e] from FUNCT_2:sch 1(A1); take f; let o be Element of C; thus thesis by A2; end; uniqueness proof let F1,F2 be Function of the carrier of C,the carrier of ConceptLattice(C); assume A3: for o being Element of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st F1.o = ConceptStr(#O,A #) & O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = ( ObjectDerivation(C)).{o}; assume A4: for o being Element of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st F2.o = ConceptStr(#O,A #) & O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = ( ObjectDerivation(C)).{o}; A5: for o being set st o in the carrier of C holds F1.o = F2.o proof let o be set; assume o in the carrier of C; then reconsider o as Element of C; (ex O being Subset of the carrier of C, A being Subset of the carrier' of C st F1.o = ConceptStr(#O,A#) & O = (AttributeDerivation(C)) .(( ObjectDerivation(C) ).{o}) & A = (ObjectDerivation(C)).{o} )& ex O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st F2.o = ConceptStr(#O9,A9#) & O9 = (AttributeDerivation( C)).((ObjectDerivation(C)).{o} ) & A9 = (ObjectDerivation (C)).{o} by A3,A4; hence thesis; end; dom F1 = the carrier of C & dom F2 = the carrier of C by FUNCT_2:def 1; hence thesis by A5,FUNCT_1:2; end; end; definition let C be FormalContext; func delta(C) -> Function of the carrier' of C, the carrier of ConceptLattice(C) means :Def5: for a being Element of the carrier' of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st it.a = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).{a} & A = ( ObjectDerivation(C)).((AttributeDerivation(C)).{a}); existence proof defpred P[set, set] means ex O being Subset of the carrier of C, A being Subset of the carrier' of C st $2 = ConceptStr(#O,A#) & O = ( AttributeDerivation(C)).{$1} & A = (ObjectDerivation(C)).((AttributeDerivation( C)).{$1}); A1: for e being set st e in the carrier' of C ex u being set st u in the carrier of ConceptLattice(C) & P[e,u] proof let e be set; assume e in the carrier' of C; then reconsider se = {e} as Subset of the carrier' of C by ZFMISC_1:31; set A = (ObjectDerivation(C)).((AttributeDerivation(C)).se); set O = (AttributeDerivation(C)).se; take ConceptStr(#O,A#); ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) & ConceptStr (#O,A#) is FormalConcept of C by CONLAT_1:21,def 20; hence thesis by CONLAT_1:31; end; consider f being Function of the carrier' of C, the carrier of ConceptLattice(C) such that A2: for e being set st e in the carrier' of C holds P[e,f.e] from FUNCT_2:sch 1(A1); take f; let o be Element of the carrier' of C; thus thesis by A2; end; uniqueness proof let F1,F2 be Function of the carrier' of C,the carrier of ConceptLattice(C ); assume A3: for a being Element of the carrier' of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st F1.a = ConceptStr(# O,A#) & O = (AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).(( AttributeDerivation(C)).{a}); assume A4: for a being Element of the carrier' of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st F2.a = ConceptStr(# O,A#) & O = (AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).(( AttributeDerivation(C)).{a}); A5: for a being set st a in the carrier' of C holds F1.a = F2.a proof let a be set; assume a in the carrier' of C; then reconsider a as Element of the carrier' of C; (ex O being Subset of the carrier of C, A being Subset of the carrier' of C st F1.a = ConceptStr(#O,A#) & O = (AttributeDerivation(C)) .{a} & A = ( ObjectDerivation(C)).((AttributeDerivation(C)).{a}) )& ex O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st F2.a = ConceptStr (# O9,A9#) & O9 = (AttributeDerivation( C)).{a} & A9 = (ObjectDerivation(C)).(( AttributeDerivation(C)).{a}) by A3,A4; hence thesis; end; dom F1 = the carrier' of C & dom F2 = the carrier' of C by FUNCT_2:def 1; hence thesis by A5,FUNCT_1:2; end; end; theorem for C being FormalContext for o being Object of C for a being Attribute of C holds (gamma(C)).o is FormalConcept of C & (delta(C)).a is FormalConcept of C proof let C be FormalContext; let o be Object of C; let a be Attribute of C; ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by CONLAT_1:def 20; hence thesis by CONLAT_1:def 15; end; theorem Th12: for C being FormalContext holds rng(gamma(C)) is supremum-dense & rng(delta(C)) is infimum-dense proof let C be FormalContext; set G = rng(gamma(C)); thus G is supremum-dense proof let a be Element of ConceptLattice(C); A1: {ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st o in the Extent of a@ & O = ( AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (ObjectDerivation(C)) .{o}} c= G proof let x be set; assume x in {ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st o in the Extent of a @ & O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = ( ObjectDerivation(C)).{o}}; then consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A2: x = ConceptStr(#O,A#) and A3: ex o being Object of C st o in the Extent of a@ & O = ( AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (ObjectDerivation(C)) .{o}; consider o being Object of C such that o in the Extent of a@ and O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) and A4: A = (ObjectDerivation(C)).{o} by A3; consider y being Element of ConceptLattice(C) such that A5: (gamma(C)).o = y; dom(gamma(C)) = the carrier of C & ex O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st y = ConceptStr(#O9,A9#) & O9 = ( AttributeDerivation(C)) .((ObjectDerivation(C)).{o}) & A9 = (ObjectDerivation( C)).{o} by A5,Def4,FUNCT_2:def 1; hence thesis by A2,A3,A4,A5,FUNCT_1:def 3; end; "\/"({ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st o in the Extent of a@ & O = ( AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = ( ObjectDerivation(C)) .{o}}, ConceptLattice(C)) = a@ & a = a@ by Th9, CONLAT_1:def 21; hence thesis by A1; end; let b be Element of ConceptLattice(C); set G = rng(delta(C)); A6: {ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st a in the Intent of b@ & O = ( AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((AttributeDerivation(C )).{a})} c= G proof let x be set; assume x in {ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st a in the Intent of b@ & O = (AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).(( AttributeDerivation(C)).{a})}; then consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A7: x = ConceptStr(#O,A#) and A8: ex a being Attribute of C st a in the Intent of b@ & O = ( AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((AttributeDerivation(C )).{a}); consider a being Attribute of C such that a in the Intent of b@ and A9: O = (AttributeDerivation(C)).{a} and A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by A8; consider y being Element of ConceptLattice(C) such that A10: (delta(C)).a = y; dom(delta(C)) = the carrier' of C & ex O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st y = ConceptStr(#O9,A9#) & O9 = ( AttributeDerivation(C)) .{a} & A9 = (ObjectDerivation(C)).(( AttributeDerivation(C)).{a}) by A10,Def5,FUNCT_2:def 1; hence thesis by A7,A8,A9,A10,FUNCT_1:def 3; end; "/\"({ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st a in the Intent of b @ & O = ( AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).(( AttributeDerivation(C )).{a})}, ConceptLattice(C)) = b@ & b = b@ by Th10, CONLAT_1:def 21; hence thesis by A6; end; theorem Th13: for C being FormalContext for o being Object of C for a being Attribute of C holds o is-connected-with a iff (gamma(C)).o [= (delta(C)).a proof let C be FormalContext; let o be Object of C; let a be Attribute of C; set aa = {a}; set o9 = {o}; set oo = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}); consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A1: (gamma(C)).o = ConceptStr(#O,A#) and A2: O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) and A = (ObjectDerivation(C)).{o} by Def4; hereby assume o is-connected-with a; then a in {a9 where a9 is Attribute of C : o is-connected-with a9}; then a in (ObjectDerivation(C)).({o}) by CONLAT_1:1; then A3: {a} c= (ObjectDerivation(C)).({o}) by ZFMISC_1:31; consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A4: (gamma(C)).o = ConceptStr(#O,A#) and A5: O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) and A = (ObjectDerivation(C)).{o} by Def4; consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that A6: (delta(C)).a = ConceptStr(#O9,A9#) and A7: O9 = (AttributeDerivation(C)).{a} and A9 = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by Def5; A8: the Extent of ((delta(C)).a)@ = O9 by A6,CONLAT_1:def 21; the Extent of ((gamma(C)).o)@ = O by A4,CONLAT_1:def 21; then the Extent of ((gamma(C)).o)@ c= the Extent of ((delta(C)).a)@ by A3,A5,A7 ,A8,CONLAT_1:4; then ((gamma(C)).o)@ is-SubConcept-of ((delta(C)).a)@ by CONLAT_1:def 16; hence ((gamma(C)).o) [= ((delta(C)).a) by CONLAT_1:43; end; consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that A9: (delta(C)).a = ConceptStr(#O9,A9#) and A10: O9 = (AttributeDerivation(C)).{a} and A9 = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by Def5; assume ((gamma(C)).o) [= ((delta(C)).a); then ((gamma(C)).o)@ is-SubConcept-of ((delta(C)).a)@ by CONLAT_1:43; then A11: the Extent of ((gamma(C)).o)@ c= the Extent of ((delta(C)).a)@ by CONLAT_1:def 16; the Extent of ((delta(C)).a)@ = O9 by A9,CONLAT_1:def 21; then O c= O9 by A11,A1,CONLAT_1:def 21; then aa c= (ObjectDerivation(C)).oo by A2,A10,CONLAT_1:11; then {a} c= (ObjectDerivation(C)).o9 by CONLAT_1:7; then a in (ObjectDerivation(C)).({o}) by ZFMISC_1:31; then a in {a9 where a9 is Attribute of C : o is-connected-with a9} by CONLAT_1:1; then ex b being Attribute of C st b = a & o is-connected-with b; hence thesis; end; begin :: The Characterization Lm1: for L1,L2 being Lattice for f being Function of the carrier of L1, the carrier of L2 holds (for a,b being Element of L1 holds f.a [= f.b implies a [= b) implies f is one-to-one proof let L1,L2 be Lattice; let f be Function of the carrier of L1, the carrier of L2; assume A1: for a,b being Element of L1 holds f.a [= f.b implies a [= b; let x,y be set; assume that A2: x in dom f and A3: y in dom f and A4: f.x = f.y; reconsider y as Element of L1 by A3; reconsider x as Element of L1 by A2; x [= y & y [= x by A1,A4; hence thesis by LATTICES:8; end; Lm2: for L1,L2 being complete Lattice for f being Function of the carrier of L1, the carrier of L2 st f is one-to-one & rng f = the carrier of L2 holds (for a,b being Element of L1 holds a [= b iff f.a [= f.b) implies f is Homomorphism of L1,L2 proof let L1,L2 be complete Lattice; let f be Function of the carrier of L1, the carrier of L2; assume A1: f is one-to-one & rng f = the carrier of L2; assume A2: for a,b being Element of L1 holds a [= b iff f.a [= f.b; A3: for a,b being Element of L1 holds f.(a "/\" b) = f.a "/\" f.b proof let a,b be Element of L1; a "/\" b [= b by LATTICES:6; then A4: f.(a "/\" b) [= f.b by A2; A5: for r being Element of L2 st r is_less_than {f.a,f.b} holds r [= f.(a "/\" b) proof reconsider g = f" as Function of the carrier of L2, the carrier of L1 by A1,FUNCT_2:25; let r be Element of L2; assume A6: r is_less_than {f.a,f.b}; A7: f.(g.r) = r by A1,FUNCT_1:35; f.b in {f.a,f.b} by TARSKI:def 2; then r [= f.b by A6,LATTICE3:def 16; then A8: g.r [= b by A2,A7; f.a in {f.a,f.b} by TARSKI:def 2; then r [= f.a by A6,LATTICE3:def 16; then g.r [= a by A2,A7; then for q being Element of L1 st q in {a,b} holds g.r [= q by A8, TARSKI:def 2; then A9: g.r is_less_than {a,b} by LATTICE3:def 16; a "/\" b = "/\"{a,b} by LATTICE3:43; then g.r [= a "/\" b by A9,LATTICE3:34; hence thesis by A2,A7; end; a "/\" b [= a by LATTICES:6; then f.(a "/\" b) [= f.a by A2; then for q being Element of L2 st q in {f.a,f.b} holds f.(a "/\" b) [= q by A4,TARSKI:def 2; then f.(a "/\" b) is_less_than {f.a,f.b} by LATTICE3:def 16; then f.(a "/\" b) = "/\"({f.a,f.b},L2) by A5,LATTICE3:34; hence thesis by LATTICE3:43; end; for a,b being Element of L1 holds f.(a "\/" b) = f.a "\/" f.b proof let a,b be Element of L1; b [= a "\/" b by LATTICES:5; then A10: f.b [= f.(a "\/" b) by A2; A11: for r being Element of L2 st {f.a,f.b} is_less_than r holds f.(a "\/" b) [= r proof reconsider g = f" as Function of the carrier of L2, the carrier of L1 by A1,FUNCT_2:25; let r be Element of L2; assume A12: {f.a,f.b} is_less_than r; A13: f.(g.r) = r by A1,FUNCT_1:35; f.b in {f.a,f.b} by TARSKI:def 2; then f.b [= r by A12,LATTICE3:def 17; then A14: b [= g.r by A2,A13; f.a in {f.a,f.b} by TARSKI:def 2; then f.a [= r by A12,LATTICE3:def 17; then a [= g.r by A2,A13; then for q being Element of L1 st q in {a,b} holds q [= g.r by A14, TARSKI:def 2; then A15: {a,b} is_less_than g.r by LATTICE3:def 17; a "\/" b = "\/"{a,b} by LATTICE3:43; then a "\/" b [= g.r by A15,LATTICE3:def 21; hence thesis by A2,A13; end; a [= a "\/" b by LATTICES:5; then f.a [= f.(a "\/" b) by A2; then for q being Element of L2 st q in {f.a,f.b} holds q [= f.(a "\/" b) by A10, TARSKI:def 2; then {f.a,f.b} is_less_than f.(a "\/" b) by LATTICE3:def 17; then f.(a "\/" b) = "\/"({f.a,f.b},L2) by A11,LATTICE3:def 21; hence thesis by LATTICE3:43; end; hence thesis by A3,LATTICE4:def 1; end; Lm3: for C being FormalContext for CS being ConceptStr over C st ( ObjectDerivation(C)).(the Extent of CS) = the Intent of CS holds CS is non empty proof let C be FormalContext; let CS be ConceptStr over C; assume A1: (ObjectDerivation(C)).(the Extent of CS) = the Intent of CS; per cases; suppose the Extent of CS is empty; then the Intent of CS = the carrier' of C by A1,CONLAT_1:17; hence thesis by CONLAT_1:def 8; end; suppose the Extent of CS is non empty; hence thesis by CONLAT_1:def 8; end; end; theorem Th14: for L being complete Lattice for C being FormalContext holds ConceptLattice(C),L are_isomorphic iff ex g being Function of the carrier of C, the carrier of L, d being Function of the carrier' of C, the carrier of L st rng(g) is supremum-dense & rng(d) is infimum-dense & for o being Object of C, a being Attribute of C holds o is-connected-with a iff g.o [= d.a proof let L be complete Lattice; let C be FormalContext; hereby assume ConceptLattice(C),L are_isomorphic; then consider f being Homomorphism of ConceptLattice(C),L such that A1: f is bijective by LATTICE4:def 2; take g = f * gamma(C), d = f * delta(C); thus rng(g) is supremum-dense proof let a be Element of L; consider b being Element of ConceptLattice(C) such that A2: a = f.b by A1,LATTICE4:6; rng(gamma(C)) is supremum-dense by Th12; then consider D9 being Subset of rng(gamma(C)) such that A3: b = "\/"(D9,ConceptLattice(C)) by LATTICE6:def 13; set D = {f.x where x is Element of ConceptLattice(C) : x in D9}; A4: for r being Element of L st D is_less_than r holds a [= r proof let r be Element of L; consider r9 being Element of ConceptLattice(C) such that A5: r = f.r9 by A1,LATTICE4:6; reconsider r9 as Element of ConceptLattice(C); assume A6: D is_less_than r; for q being Element of ConceptLattice(C) st q in D9 holds q [= r9 proof let q be Element of ConceptLattice(C); assume q in D9; then f.q in {f.x where x is Element of ConceptLattice(C) : x in D9}; then f.q [= f.r9 by A6,A5,LATTICE3:def 17; hence thesis by A1,LATTICE4:5; end; then D9 is_less_than r9 by LATTICE3:def 17; then b [= r9 by A3,LATTICE3:def 21; hence thesis by A1,A2,A5,LATTICE4:5; end; A7: D c= rng(g) proof let x be set; assume x in D; then consider x9 being Element of ConceptLattice(C) such that A8: x = f.x9 and A9: x9 in D9; consider y being set such that A10: y in dom(gamma(C)) & (gamma(C)).y = x9 by A9,FUNCT_1:def 3; dom f = the carrier of ConceptLattice(C) by FUNCT_2:def 1; then A11: y in dom(f * (gamma(C))) by A10,FUNCT_1:11; x = (f * (gamma(C))).y by A8,A10,FUNCT_1:13; hence thesis by A11,FUNCT_1:def 3; end; A12: D9 is_less_than b by A3,LATTICE3:def 21; D is_less_than a proof let q be Element of L; assume q in D; then consider q9 being Element of ConceptLattice(C) such that A13: q = f.q9 and A14: q9 in D9; q9 [= b by A12,A14,LATTICE3:def 17; hence thesis by A1,A2,A13,LATTICE4:5; end; then a = "\/"(D,L) by A4,LATTICE3:def 21; hence thesis by A7; end; thus rng(d) is infimum-dense proof let a be Element of L; consider b being Element of ConceptLattice(C) such that A15: a = f.b by A1,LATTICE4:6; rng(delta(C)) is infimum-dense by Th12; then consider D9 being Subset of rng(delta(C)) such that A16: b = "/\"(D9,ConceptLattice(C)) by LATTICE6:def 14; set D = {f.x where x is Element of ConceptLattice(C) : x in D9}; A17: for r being Element of L st r is_less_than D holds r [= a proof let r be Element of L; consider r9 being Element of ConceptLattice(C) such that A18: r = f.r9 by A1,LATTICE4:6; reconsider r9 as Element of ConceptLattice(C); assume A19: r is_less_than D; r9 is_less_than D9 proof let q be Element of ConceptLattice(C); assume q in D9; then f.q in {f.x where x is Element of ConceptLattice(C) : x in D9}; then f.r9 [= f.q by A19,A18,LATTICE3:def 16; hence thesis by A1,LATTICE4:5; end; then r9 [= b by A16,LATTICE3:34; hence thesis by A1,A15,A18,LATTICE4:5; end; A20: D c= rng(d) proof let x be set; assume x in D; then consider x9 being Element of ConceptLattice(C) such that A21: x = f.x9 and A22: x9 in D9; consider y being set such that A23: y in dom(delta(C)) & (delta(C)).y = x9 by A22,FUNCT_1:def 3; dom f = the carrier of ConceptLattice(C) by FUNCT_2:def 1; then A24: y in dom(f * (delta(C))) by A23,FUNCT_1:11; x = (f * (delta(C))).y by A21,A23,FUNCT_1:13; hence thesis by A24,FUNCT_1:def 3; end; A25: b is_less_than D9 by A16,LATTICE3:34; a is_less_than D proof let q be Element of L; assume q in D; then consider q9 being Element of ConceptLattice(C) such that A26: q = f.q9 and A27: q9 in D9; b [= q9 by A25,A27,LATTICE3:def 16; hence thesis by A1,A15,A26,LATTICE4:5; end; then a = "/\"(D,L) by A17,LATTICE3:34; hence thesis by A20; end; let o be Object of C, a be Attribute of C; A28: o is-connected-with a iff (gamma(C)).o [= (delta(C)).a by Th13; hereby dom(delta(C)) = the carrier' of C by FUNCT_2:def 1; then A29: f.((delta(C)).a) = (f * (delta(C))).a by FUNCT_1:13; dom(gamma(C)) = the carrier of C by FUNCT_2:def 1; then A30: f.((gamma(C)).o) = (f * (gamma(C))).o by FUNCT_1:13; assume o is-connected-with a; hence g.o [= d.a by A1,A28,A30,A29,LATTICE4:5; end; dom(gamma(C)) = the carrier of C by FUNCT_2:def 1; then A31: f.((gamma(C)).o) = (f * (gamma(C))).o by FUNCT_1:13; dom(delta(C)) = the carrier' of C by FUNCT_2:def 1; then A32: f.((delta(C)).a) = (f * (delta(C))).a by FUNCT_1:13; assume g.o [= d.a; then (gamma(C)).o [= (delta(C)).a by A1,A31,A32,LATTICE4:5; hence o is-connected-with a by Th13; end; given g being Function of the carrier of C, the carrier of L, d being Function of the carrier' of C, the carrier of L such that A33: rng(g) is supremum-dense and A34: rng(d) is infimum-dense and A35: for o being Object of C, a being Attribute of C holds o is-connected-with a iff g.o [= d.a; set fi = {[x,ConceptStr(#O,A#)] where x is Element of L, O is Subset of the carrier of C, A is Subset of the carrier' of C : O = {o where o is Object of C : g.o [= x} & A = {a where a is Attribute of C : x [= d.a} }; set f = {[ConceptStr(#O,A#),x] where O is Subset of the carrier of C, A is Subset of the carrier' of C, x is Element of L : ConceptStr(#O,A#) is FormalConcept of C & x = "\/"({g.o where o is Object of C : o in O},L) }; A36: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by CONLAT_1:def 20; A37: f c= [:the carrier of ConceptLattice(C), the carrier of L:] proof let y be set; assume y in f; then consider O being Subset of the carrier of C, A being Subset of the carrier' of C, x being Element of L such that A38: y = [ConceptStr(#O,A#),x] and A39: ConceptStr(#O,A#) is FormalConcept of C and x = "\/"({g.o where o is Object of C : o in O},L); ConceptStr(#O,A#) in the carrier of ConceptLattice(C) by A36,A39, CONLAT_1:31; hence thesis by A38,ZFMISC_1:def 2; end; fi c= [:the carrier of L, the carrier of ConceptLattice(C):] proof let y be set; assume y in fi; then consider x being Element of L, O being Subset of the carrier of C, A being Subset of the carrier' of C such that A40: y = [x,ConceptStr(#O,A#)] and A41: O = {o where o is Object of C : g.o [= x} and A42: A = {a where a is Attribute of C : x [= d.a}; A43: (AttributeDerivation(C)).(the Intent of ConceptStr(#O,A#)) = the Extent of ConceptStr(#O,A#) proof thus (AttributeDerivation(C)). (the Intent of ConceptStr(#O,A#)) c= the Extent of ConceptStr(#O,A#) proof let u be set; A44: "/\"({d.a9 where a9 is Attribute of C : x [= d.a9},L) = x proof consider D being Subset of rng(d) such that A45: "/\"(D,L) = x by A34,LATTICE6:def 14; A46: x is_less_than D by A45,LATTICE3:34; D c= {d.a9 where a9 is Attribute of C : x [= d.a9} proof let u be set; assume A47: u in D; then consider v being set such that A48: v in dom d and A49: u = d.v by FUNCT_1:def 3; reconsider v as Attribute of C by A48; x [= d.v by A46,A47,A49,LATTICE3:def 16; hence thesis by A49; end; then A50: "/\"({d.a9 where a9 is Attribute of C : x [= d.a9},L) [= x by A45, LATTICE3:45; x is_less_than {d.a9 where a9 is Attribute of C : x [= d.a9} proof let u be Element of L; assume u in {d.a9 where a9 is Attribute of C : x [= d.a9}; then ex v being Attribute of C st u = d.v & x [= d.v; hence thesis; end; then x [= "/\"({d.a9 where a9 is Attribute of C : x [= d.a9},L) by LATTICE3:39; hence thesis by A50,LATTICES:8; end; assume u in (AttributeDerivation(C)).(the Intent of ConceptStr(#O,A #)); then u in { o where o is Object of C : for a being Attribute of C st a in the Intent of ConceptStr(#O,A#) holds o is-connected-with a } by CONLAT_1:def 4; then consider u9 being Object of C such that A51: u9 = u and A52: for a being Attribute of C st a in the Intent of ConceptStr (#O,A#) holds u9 is-connected-with a; A53: for v being Attribute of C st v in {a where a is Attribute of C: x [= d.a} holds g.u9 [= d.v proof let v be Attribute of C; assume v in {a where a is Attribute of C : x [= d.a}; then u9 is-connected-with v by A42,A52; hence thesis by A35; end; g.u9 is_less_than {d.a where a is Attribute of C: x [= d.a} proof let q be Element of L; assume q in {d.a where a is Attribute of C: x [= d.a}; then consider b being Attribute of C such that A54: q = d.b and A55: x [= d.b; b in {a where a is Attribute of C: x [= d.a} by A55; hence thesis by A53,A54; end; then g.u9 [= x by A44,LATTICE3:34; hence thesis by A41,A51; end; let u be set; assume u in the Extent of ConceptStr(#O,A#); then consider u9 being Object of C such that A56: u9 = u and A57: g.u9 [= x by A41; A58: for v being Attribute of C st v in {a where a is Attribute of C: x [= d.a} holds g.u9 [= d.v proof let v be Attribute of C; assume v in {a where a is Attribute of C : x [= d.a}; then ex v9 being Attribute of C st v9 = v & x [= d.v9; hence thesis by A57,LATTICES:7; end; for v being Attribute of C st v in {a where a is Attribute of C: x [= d.a} holds u9 is-connected-with v proof let v be Attribute of C; assume v in {a where a is Attribute of C : x [= d.a}; then g.u9 [= d.v by A58; hence thesis by A35; end; then u9 in {o where o is Object of C : for a being Attribute of C st a in the Intent of ConceptStr(#O,A#) holds o is-connected-with a } by A42; hence thesis by A56,CONLAT_1:def 4; end; (ObjectDerivation(C)).(the Extent of ConceptStr(#O,A#)) = the Intent of ConceptStr(#O,A#) proof thus (ObjectDerivation(C)). (the Extent of ConceptStr(#O,A#)) c= the Intent of ConceptStr(#O,A#) proof let u be set; A59: "\/"({g.a9 where a9 is Object of C : g.a9 [= x},L) = x proof consider D being Subset of rng(g) such that A60: "\/"(D,L) = x by A33,LATTICE6:def 13; A61: D is_less_than x by A60,LATTICE3:def 21; D c= {g.a9 where a9 is Object of C : g.a9 [= x} proof let u be set; assume A62: u in D; then consider v being set such that A63: v in dom g and A64: u = g.v by FUNCT_1:def 3; reconsider v as Object of C by A63; g.v [= x by A61,A62,A64,LATTICE3:def 17; hence thesis by A64; end; then A65: x [= "\/"({g.a9 where a9 is Object of C : g.a9 [= x},L ) by A60, LATTICE3:45; {g.a9 where a9 is Object of C : g.a9 [= x} is_less_than x proof let u be Element of L; assume u in {g.a9 where a9 is Object of C : g.a9 [= x}; then ex v being Object of C st u = g.v & g.v [= x; hence thesis; end; then "\/"({g.a9 where a9 is Object of C : g.a9 [= x},L) [= x by LATTICE3:def 21; hence thesis by A65,LATTICES:8; end; assume u in (ObjectDerivation(C)).(the Extent of ConceptStr(#O,A#)); then u in { o where o is Attribute of C : for a being Object of C st a in the Extent of ConceptStr(#O,A#) holds a is-connected-with o } by CONLAT_1:def 3; then consider u9 being Attribute of C such that A66: u9 = u and A67: for a being Object of C st a in the Extent of ConceptStr(#O, A#) holds a is-connected-with u9; A68: for v being Object of C st v in {a where a is Object of C: g.a [= x} holds g.v [= d.u9 proof let v be Object of C; assume v in {a where a is Object of C : g.a [= x}; then v is-connected-with u9 by A41,A67; hence thesis by A35; end; {g.a where a is Object of C: g.a [= x} is_less_than d.u9 proof let q be Element of L; assume q in {g.a where a is Object of C: g.a [= x}; then consider b being Object of C such that A69: q = g.b and A70: g.b [= x; b in {a where a is Object of C: g.a [= x} by A70; hence thesis by A68,A69; end; then x [= d.u9 by A59,LATTICE3:def 21; hence thesis by A42,A66; end; let u be set; assume u in the Intent of ConceptStr(#O,A#); then consider u9 being Attribute of C such that A71: u9 = u and A72: x [= d.u9 by A42; A73: for v being Object of C st v in {a where a is Object of C: g.a [= x} holds g.v [= d.u9 proof let v be Object of C; assume v in {a where a is Object of C : g.a [= x}; then ex v9 being Object of C st v9 = v & g.v9 [= x; hence thesis by A72,LATTICES:7; end; for v being Object of C st v in {a where a is Object of C : g.a [= x} holds v is-connected-with u9 proof let v be Object of C; assume v in {a where a is Object of C : g.a [= x}; then g.v [= d.u9 by A73; hence thesis by A35; end; then u9 in {o where o is Attribute of C : for a being Object of C st a in the Extent of ConceptStr(#O,A#) holds a is-connected-with o } by A41; hence thesis by A71,CONLAT_1:def 3; end; then ConceptStr(#O,A#) is FormalConcept of C by A43,Lm3,CONLAT_1:def 10; then ConceptStr(#O,A#) in the carrier of ConceptLattice(C) by A36, CONLAT_1:31; hence thesis by A40,ZFMISC_1:def 2; end; then reconsider fi as Relation of the carrier of L, the carrier of ConceptLattice (C); A74: for x,y1,y2 being set st [x,y1] in fi & [x,y2] in fi holds y1 = y2 proof let x,y1,y2 be set; assume that A75: [x,y1] in fi and A76: [x,y2] in fi; consider z being Element of L, O being Subset of the carrier of C, A being Subset of the carrier' of C such that A77: [x,y1] = [z,ConceptStr(#O,A#)] and A78: O = {o where o is Object of C : g.o [= z} & A = {a where a is Attribute of C : z [= d.a} by A75; consider z9 being Element of L, O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that A79: [x,y2] = [z9,ConceptStr(#O9,A9#)] and A80: O9 = {o where o is Object of C : g.o [= z9} & A9 = {a where a is Attribute of C : z9 [= d.a} by A76; A81: z = x by A77,XTUPLE_0:1 .= z9 by A79,XTUPLE_0:1; thus y1 = [x,y1]`2 .= [x,y2]`2 by A77,A78,A79,A80,A81 .= y2; end; the carrier of L c= dom fi proof let y be set; assume y in the carrier of L; then reconsider y as Element of L; set A = {a where a is Attribute of C : y [= d.a}; A c= the carrier' of C proof let u be set; assume u in A; then ex u9 being Attribute of C st u9 = u & y [= d.u9; hence thesis; end; then reconsider A as Subset of the carrier' of C; set O = {o where o is Object of C : g.o [= y}; O c= the carrier of C proof let u be set; assume u in O; then ex u9 being Object of C st u9 = u & g.u9 [= y; hence thesis; end; then reconsider O as Subset of the carrier of C; [y,ConceptStr(#O,A#)] in fi; hence thesis by XTUPLE_0:def 12; end; then A82: the carrier of L = dom fi by XBOOLE_0:def 10; reconsider f as Relation of the carrier of ConceptLattice(C), the carrier of L by A37; the carrier of ConceptLattice(C) c= dom f proof let y be set; assume y in the carrier of ConceptLattice(C); then A83: y is strict FormalConcept of C by A36,CONLAT_1:31; then consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that A84: y = ConceptStr(#O9,A9#); reconsider z = "\/"({g.o where o is Object of C : o in O9},L) as Element of L; [y,z] in f by A83,A84; hence thesis by XTUPLE_0:def 12; end; then A85: the carrier of ConceptLattice(C) = dom f by XBOOLE_0:def 10; reconsider fi as Function of the carrier of L, the carrier of ConceptLattice (C) by A82,A74,FUNCT_1:def 1,FUNCT_2:def 1; for x,y1,y2 being set st [x,y1] in f & [x,y2] in f holds y1 = y2 proof let x,y1,y2 be set; assume that A86: [x,y1] in f and A87: [x,y2] in f; consider O being Subset of the carrier of C, A being Subset of the carrier' of C, z being Element of L such that A88: [x,y1] = [ConceptStr(#O,A#),z] and ConceptStr(#O,A#) is FormalConcept of C and A89: z = "\/"({g.o where o is Object of C : o in O},L) by A86; consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C, z9 being Element of L such that A90: [x,y2] = [ConceptStr(#O9,A9#),z9] and ConceptStr(#O9,A9#) is FormalConcept of C and A91: z9 = "\/"({g.o where o is Object of C : o in O9},L) by A87; A92: ConceptStr(#O,A#) = [ConceptStr(#O,A#),z]`1 .= [x,y1]`1 by A88 .= x .= [x,y2]`1 .= [ConceptStr(#O9,A9#),z9]`1 by A90 .= ConceptStr(#O9,A9#); thus y1 = [x,y1]`2 .= [x,y2]`2 by A88,A89,A90,A91,A92 .= y2; end; then reconsider f as Function of the carrier of ConceptLattice(C), the carrier of L by A85,FUNCT_1:def 1,FUNCT_2:def 1; A93: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by CONLAT_1:def 20; A94: for a being Element of L holds f.(fi.a) = a proof let a be Element of L; reconsider a as Element of L; set A = {a9 where a9 is Attribute of C : a [= d.a9}; A c= the carrier' of C proof let u be set; assume u in A; then ex u9 being Attribute of C st u9 = u & a [= d.u9; hence thesis; end; then reconsider A as Subset of the carrier' of C; set O = {o where o is Object of C : g.o [= a}; O c= the carrier of C proof let u be set; assume u in O; then ex u9 being Object of C st u9 = u & g.u9 [= a; hence thesis; end; then reconsider O as Subset of the carrier of C; set b = "\/"({g.o where o is Object of C : o in the Extent of ConceptStr(# O,A#)},L); A95: "\/"({g.o where o is Object of C : o in {o9 where o9 is Object of C : g.o9 [= a}},L) = a proof consider D being Subset of rng(g) such that A96: "\/"(D,L) = a by A33,LATTICE6:def 13; A97: D is_less_than a by A96,LATTICE3:def 21; D c= {g.o where o is Object of C : o in {o9 where o9 is Object of C: g.o9 [= a}} proof let u be set; assume A98: u in D; then consider v being set such that A99: v in dom g and A100: u = g.v by FUNCT_1:def 3; reconsider v as Object of C by A99; g.v [= a by A97,A98,A100,LATTICE3:def 17; then v in {o9 where o9 is Object of C : g.o9 [= a}; hence thesis by A100; end; then A101: a [= "\/"({g.o where o is Object of C : o in {o9 where o9 is Object of C : g.o9 [= a}},L) by A96,LATTICE3:45; {g.o where o is Object of C : o in {o9 where o9 is Object of C : g .o9 [= a}} is_less_than a proof let u be Element of L; assume u in {g.o where o is Object of C : o in {o9 where o9 is Object of C : g.o9 [= a}}; then consider v being Object of C such that A102: u = g.v and A103: v in {o9 where o9 is Object of C : g.o9 [= a}; ex ov being Object of C st ov = v & g.ov [= a by A103; hence thesis by A102; end; then "\/"({g.o where o is Object of C : o in {o9 where o9 is Object of C: g.o9 [= a}},L) [= a by LATTICE3:def 21; hence thesis by A101,LATTICES:8; end; A104: [a,ConceptStr(#O,A#)] in fi; then ConceptStr(#O,A#) in rng(fi) by XTUPLE_0:def 13; then ConceptStr(#O,A#) is FormalConcept of C by A93,CONLAT_1:31; then [ConceptStr(#O,A#),b] in f; then f.ConceptStr(#O,A#) = b by FUNCT_1:1; hence thesis by A104,A95,FUNCT_1:1; end; the carrier of L c= rng f proof let u be set; A105: dom f = the carrier of ConceptLattice(C) by FUNCT_2:def 1; assume A106: u in the carrier of L; then u in dom fi by FUNCT_2:def 1; then consider v being set such that A107: [u,v] in fi by XTUPLE_0:def 12; reconsider u as Element of L by A106; v in rng fi by A107,XTUPLE_0:def 13; then reconsider v as Element of ConceptLattice(C); f.v = f.(fi.u) by A107,FUNCT_1:1 .= u by A94; hence thesis by A105,FUNCT_1:def 3; end; then A108: rng f = the carrier of L by XBOOLE_0:def 10; A109: for x being Element of ConceptLattice(C) holds f.x = "/\"({d.a where a is Attribute of C : a in the Intent of x@},L) proof let x be Element of ConceptLattice(C); set y = "\/"({g.o where o is Object of C : o in the Extent of x@},L); A110: [x@, y] in f; A111: for o being set holds o in {d.a9 where a9 is Attribute of C : y [= d .a9} implies o in {d.a where a is Attribute of C : a in the Intent of x@} proof let o be set; assume o in {d.a9 where a9 is Attribute of C : y [= d.a9}; then consider u being Attribute of C such that A112: o = d.u and A113: y [= d.u; A114: for o being Object of C st o in the Extent of x@ holds g.o [= d.u proof let o be Object of C; assume o in the Extent of x@; then g.o in {g.o9 where o9 is Object of C : o9 in the Extent of x @}; then g.o [= y by LATTICE3:38; hence thesis by A113,LATTICES:7; end; for o being Object of C st o in the Extent of x@ holds o is-connected-with u proof let o be Object of C; assume o in the Extent of x@; then g.o [= d.u by A114; hence thesis by A35; end; then u in {a9 where a9 is Attribute of C : for o9 being Object of C st o9 in the Extent of x@ holds o9 is-connected-with a9}; then u in (ObjectDerivation(C)).(the Extent of x@) by CONLAT_1:def 3; then u in the Intent of x@ by CONLAT_1:def 10; hence thesis by A112; end; A115: for o9 being Object of C st o9 in the Extent of x@ for a9 being Attribute of C st a9 in the Intent of x@ holds g.o9 [= d.a9 proof let o9 be Object of C; assume A116: o9 in the Extent of x@; let a9 be Attribute of C; assume a9 in the Intent of x@; then a9 in (ObjectDerivation(C)).(the Extent of x@) by CONLAT_1:def 10; then a9 in {a where a is Attribute of C : for o being Object of C st o in the Extent of x@ holds o is-connected-with a } by CONLAT_1:def 3; then ex aa being Attribute of C st aa = a9 & for o being Object of C st o in the Extent of x@ holds o is-connected-with aa; then o9 is-connected-with a9 by A116; hence thesis by A35; end; A117: for o being set holds o in {d.a where a is Attribute of C : a in the Intent of x@} implies o in {d.a9 where a9 is Attribute of C : y [= d.a9} proof let o be set; assume o in {d.a where a is Attribute of C : a in the Intent of x@}; then consider b being Attribute of C such that A118: o = d.b and A119: b in the Intent of x@; {g.o9 where o9 is Object of C : o9 in the Extent of x@} is_less_than d.b proof let q be Element of L; assume q in {g.o9 where o9 is Object of C : o9 in the Extent of x@}; then ex u being Object of C st q = g.u & u in the Extent of x @; hence thesis by A115,A119; end; then y [= d.b by LATTICE3:def 21; hence thesis by A118; end; A120: "/\"({d.a9 where a9 is Attribute of C : y [= d.a9},L) = y proof consider D being Subset of rng(d) such that A121: "/\"(D,L) = y by A34,LATTICE6:def 14; A122: y is_less_than D by A121,LATTICE3:34; D c= {d.a9 where a9 is Attribute of C : y [= d.a9} proof let u be set; assume A123: u in D; then consider v being set such that A124: v in dom d and A125: u = d.v by FUNCT_1:def 3; reconsider v as Attribute of C by A124; y [= d.v by A122,A123,A125,LATTICE3:def 16; hence thesis by A125; end; then A126: "/\"({d.a9 where a9 is Attribute of C : y [= d.a9},L) [= y by A121, LATTICE3:45; y is_less_than {d.a9 where a9 is Attribute of C : y [= d.a9} proof let u be Element of L; assume u in {d.a9 where a9 is Attribute of C : y [= d.a9}; then ex v being Attribute of C st u = d.v & y [= d.v; hence thesis; end; then y [= "/\"({d.a9 where a9 is Attribute of C : y [= d.a9},L) by LATTICE3:39; hence thesis by A126,LATTICES:8; end; f.x = f.x@ by CONLAT_1:def 21 .= y by A110,FUNCT_1:1; hence thesis by A111,A117,A120,TARSKI:1; end; A127: for a being Element of ConceptLattice(C) holds fi.(f.a) = a proof let a be Element of ConceptLattice(C); set x = "/\"({d.u where u is Attribute of C : u in the Intent of a@},L); set A = {a9 where a9 is Attribute of C : x [= d.a9}; A c= the carrier' of C proof let u be set; assume u in A; then ex u9 being Attribute of C st u9 = u & x [= d.u9; hence thesis; end; then reconsider A as Subset of the carrier' of C; set O = {o where o is Object of C : g.o [= x}; O c= the carrier of C proof let u be set; assume u in O; then ex u9 being Object of C st u9 = u & g.u9 [= x; hence thesis; end; then reconsider O as Subset of the carrier of C; A128: O = {o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of a@ holds g.o [= d.a9 } proof thus O c= {o where o is Object of C: for a9 being Attribute of C st a9 in the Intent of a@ holds g.o [= d.a9 } proof let u be set; assume u in O; then consider o9 being Object of C such that A129: u = o9 and A130: g.o9 [= x; for a9 being Attribute of C st a9 in the Intent of a@ holds g.o9 [= d.a9 proof let a9 be Attribute of C; assume a9 in the Intent of a@; then d.a9 in {d.y where y is Attribute of C : y in the Intent of a @}; then x [= d.a9 by LATTICE3:38; hence thesis by A130,LATTICES:7; end; hence thesis by A129; end; let u be set; assume u in {o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of a@ holds g.o [= d.a9 }; then consider o9 being Object of C such that A131: o9 = u and A132: for a9 being Attribute of C st a9 in the Intent of a@ holds g. o9 [= d.a9; g.o9 is_less_than {d.y where y is Attribute of C : y in the Intent of a@} proof let q be Element of L; assume q in {d.y where y is Attribute of C : y in the Intent of a@}; then ex qa being Attribute of C st q = d.qa & qa in the Intent of a@; hence thesis by A132; end; then g.o9 [= x by LATTICE3:34; hence thesis by A131; end; {o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of a@ holds g.o [= d.a9 } = {o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of a@ holds o is-connected-with a9 } proof thus {o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of a@ holds g.o [= d.a9 } c= {o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of a@ holds o is-connected-with a9 } proof let u be set; assume u in {o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of a@ holds g.o [= d.a9 }; then consider u9 being Object of C such that A133: u = u9 and A134: for a9 being Attribute of C st a9 in the Intent of a@ holds g.u9 [= d.a9; for a9 being Attribute of C st a9 in the Intent of a@ holds u9 is-connected-with a9 proof let a9 be Attribute of C; assume a9 in the Intent of a@; then g.u9 [= d.a9 by A134; hence thesis by A35; end; hence thesis by A133; end; let u be set; assume u in {o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of a@ holds o is-connected-with a9 }; then consider u9 being Object of C such that A135: u = u9 and A136: for a9 being Attribute of C st a9 in the Intent of a@ holds u9 is-connected-with a9; for a9 being Attribute of C st a9 in the Intent of a@ holds g.u9 [= d.a9 proof let a9 be Attribute of C; assume a9 in the Intent of a@; then u9 is-connected-with a9 by A136; hence thesis by A35; end; hence thesis by A135; end; then A137: O = (AttributeDerivation(C)).(the Intent of a@) by A128,CONLAT_1:def 4 .= the Extent of a@ by CONLAT_1:def 10; A138: fi.("/\"({d.u where u is Attribute of C : u in the Intent of a@},L)) = fi.(f.a) by A109; [x,ConceptStr(#O,A#)] in fi; then A139: fi.x = ConceptStr(#O,A#) by FUNCT_1:1; then ConceptStr(#O,A#) is FormalConcept of C by A93,CONLAT_1:31; then A = (ObjectDerivation(C)).(the Extent of a@) by A137,CONLAT_1:def 10 .= the Intent of a@ by CONLAT_1:def 10; hence thesis by A138,A139,A137,CONLAT_1:def 21; end; A140: for a,b being Element of L holds a [= b implies fi.a [= fi.b proof let a,b be Element of L; set ca = fi.a, cb = fi.b; assume A141: a [= b; A142: {o where o is Object of C : g.o [= a} c= {o where o is Object of C : g.o [= b} proof let x be set; assume x in {o where o is Object of C : g.o [= a}; then consider x9 being Object of C such that A143: x9 = x and A144: g.x9 [= a; g.x9 [= b by A141,A144,LATTICES:7; hence thesis by A143; end; A145: dom fi = the carrier of L by FUNCT_2:def 1; then consider ya being set such that A146: [a,ya] in fi by XTUPLE_0:def 12; consider yb being set such that A147: [b,yb] in fi by A145,XTUPLE_0:def 12; consider xb being Element of L, Ob being Subset of the carrier of C, Ab being Subset of the carrier' of C such that A148: [b,yb] = [xb,ConceptStr(#Ob,Ab#)] and A149: Ob = {o where o is Object of C : g.o [= xb} and Ab = {a9 where a9 is Attribute of C : xb [= d.a9} by A147; A150: b = [b,yb]`1 .= [xb,ConceptStr(#Ob,Ab#)]`1 by A148 .= xb; then fi.b = ConceptStr(#Ob,Ab#) by A147,A148,FUNCT_1:1; then A151: the Extent of cb@ = Ob by CONLAT_1:def 21; consider xa being Element of L, Oa being Subset of the carrier of C, Aa being Subset of the carrier' of C such that A152: [a,ya] = [xa,ConceptStr(#Oa,Aa#)] and A153: Oa = {o where o is Object of C : g.o [= xa} and Aa = {a9 where a9 is Attribute of C : xa [= d.a9} by A146; A154: a = [a,ya]`1 .= [xa,ConceptStr(#Oa,Aa#)]`1 by A152 .= xa; then fi.a = ConceptStr(#Oa,Aa#) by A146,A152,FUNCT_1:1; then the Extent of ca@ = Oa by CONLAT_1:def 21; then ca@ is-SubConcept-of cb@ by A142,A153,A149,A154,A150,A151, CONLAT_1:def 16; hence thesis by CONLAT_1:43; end; A155: for a,b being Element of ConceptLattice(C) holds f.a [= f.b implies a [= b proof let a,b be Element of ConceptLattice(C); assume A156: f.a [= f.b; fi.(f.a) = a & fi.(f.b) = b by A127; hence thesis by A140,A156; end; for a,b being Element of ConceptLattice(C) holds a [= b implies f.a [= f.b proof let a,b be Element of ConceptLattice(C); reconsider xa = "\/"({g.o where o is Object of C : o in the Extent of a@}, L), xb = "\/"({g.o where o is Object of C : o in the Extent of b@},L) as Element of L; [a@,xa] in f; then A157: f.(a@) = xa by FUNCT_1:1; [b@,xb] in f; then A158: f.(b@) = xb by FUNCT_1:1; assume a [= b; then a@ is-SubConcept-of b@ by CONLAT_1:43; then A159: the Extent of a@ c= the Extent of b@ by CONLAT_1:def 16; A160: {g.o where o is Object of C : o in the Extent of a@} c= {g.o where o is Object of C : o in the Extent of b@} proof let x be set; assume x in {g.o where o is Object of C : o in the Extent of a@}; then ex o being Object of C st x = g.o & o in the Extent of a @; hence thesis by A159; end; a@ = a & b@ = b by CONLAT_1:def 21; hence thesis by A160,A157,A158,LATTICE3:45; end; then reconsider f as Homomorphism of ConceptLattice(C),L by A155,A108,Lm1,Lm2 ; A161: f is onto by A108,FUNCT_2:def 3; f is one-to-one by A155,Lm1; hence thesis by A161,LATTICE4:def 2; end; definition let L be Lattice; func Context(L) -> strict non quasi-empty ContextStr equals ContextStr(#the carrier of L, the carrier of L, LattRel L#); coherence by CONLAT_1:def 1; end; theorem Th15: for L being complete Lattice holds ConceptLattice(Context(L)),L are_isomorphic proof let L be complete Lattice; reconsider g = id the carrier of L as Function of the carrier of Context(L), the carrier of L; reconsider d = id the carrier of L as Function of the carrier' of Context(L) , the carrier of L; A1: for o being Object of Context(L), a being Attribute of Context(L) holds o is-connected-with a iff g.o [= d.a proof let o be Object of Context(L), a be Attribute of Context(L); reconsider o9 = o, a9 = a as Element of L; A2: g.o = o9 & d.a = a9 by FUNCT_1:17; o is-connected-with a iff [o,a] in the Information of Context(L) by CONLAT_1:def 2; hence thesis by A2,FILTER_1:31; end; for a being Element of L holds ex D9 being Subset of rng(d) st a = "/\"( D9,L) proof let a be Element of L; "/\"({a},L) = a & rng(d) = the carrier of L by LATTICE3:42,RELAT_1:45; hence thesis; end; then A3: rng(d) is infimum-dense by LATTICE6:def 14; rng(g) is supremum-dense proof let a be Element of L; "\/"({a},L) = a & rng(g) = the carrier of L by LATTICE3:42,RELAT_1:45; hence thesis; end; hence thesis by A3,A1,Th14; end; theorem for L being Lattice holds L is complete iff ex C being FormalContext st ConceptLattice(C),L are_isomorphic proof let L be Lattice; hereby assume L is complete; then ConceptLattice(Context(L)),L are_isomorphic by Th15; hence ex C being FormalContext st ConceptLattice(C),L are_isomorphic; end; given C being FormalContext such that A1: ConceptLattice(C),L are_isomorphic; let X be Subset of L; consider f being Homomorphism of L,ConceptLattice(C) such that A2: f is bijective by A1,LATTICE4:def 2; set FX = { f.x where x is Element of L : x in X }; FX c= the carrier of ConceptLattice(C) proof let x be set; assume x in FX; then ex y being Element of L st x = f.y & y in X; hence thesis; end; then reconsider FX as Subset of ConceptLattice(C); set Fa = "/\"(FX,ConceptLattice(C)); consider a being Element of L such that A3: Fa = f.a by A2,LATTICE4:6; A4: for b being Element of L st b is_less_than X holds b [= a proof let b be Element of L; assume A5: b is_less_than X; f.b is_less_than FX proof let q be Element of ConceptLattice(C); assume q in FX; then consider y being Element of L such that A6: q = f.y and A7: y in X; b [= y by A5,A7,LATTICE3:def 16; hence thesis by A2,A6,LATTICE4:5; end; then f.b [= f.a by A3,LATTICE3:34; hence thesis by A2,LATTICE4:5; end; A8: Fa is_less_than FX by LATTICE3:34; a is_less_than X proof let q be Element of L; assume q in X; then f.q in FX; then Fa [= f.q by A8,LATTICE3:def 16; hence thesis by A2,A3,LATTICE4:5; end; hence thesis by A4; end; begin :: Dual Concept Lattices registration let L be complete Lattice; cluster L.: -> complete; coherence proof let X be Subset of L.:; A1: L.: = LattStr(#the carrier of L,the L_meet of L, the L_join of L#) by LATTICE2:def 2; then reconsider X9 = X as Subset of L; set a9 = "\/"(X9,L); reconsider a = a9 as Element of L.: by A1; LattRel (L.:) = (LattRel L)~ by LATTICE3:20; then A2: LattRel (L .: .:) = ((LattRel L)~)~ by LATTICE3:20; A3: for b being Element of L.: st b is_less_than X holds b [= a proof let b be Element of L.:; reconsider b9 = b as Element of L by A1; assume A4: b is_less_than X; X9 is_less_than b9 proof let q be Element of L; reconsider q9 = q as Element of L.: by A1; assume q in X9; then b [= q9 by A4,LATTICE3:def 16; then b% <= (q9)% by LATTICE3:7; then [b%,(q9)%] in the InternalRel of LattPOSet L.: by ORDERS_2:def 5; then [(q9)%,b%] in (the InternalRel of LattPOSet L.:)~ by RELAT_1:def 7 ; then [(q9)%,b%] in the InternalRel of LattPOSet (L .: .:) by LATTICE3:20; then q% <= (b9)% by A2,ORDERS_2:def 5; hence thesis by LATTICE3:7; end; then a9 [= b9 by LATTICE3:def 21; then (a9)% <= (b9)% by LATTICE3:7; then [(a9)%,(b9)%] in the InternalRel of LattPOSet L by ORDERS_2:def 5; then [(b9)%,(a9)%] in (the InternalRel of LattPOSet L)~ by RELAT_1:def 7; then [(b9)%,(a9)%] in the InternalRel of LattPOSet (L.:) by LATTICE3:20; then b% <= a% by ORDERS_2:def 5; hence thesis by LATTICE3:7; end; A5: X9 is_less_than a9 by LATTICE3:def 21; a is_less_than X proof let q9 be Element of L.:; reconsider q = q9 as Element of L by A1; assume q9 in X; then q [= a9 by A5,LATTICE3:def 17; then q% <= (a9)% by LATTICE3:7; then [q%,(a9)%] in the InternalRel of LattPOSet L by ORDERS_2:def 5; then [(a9)%,q%] in (the InternalRel of LattPOSet L)~ by RELAT_1:def 7; then [(a9)%,q%] in the InternalRel of LattPOSet (L.:) by LATTICE3:20; then a% <= (q9)% by ORDERS_2:def 5; hence thesis by LATTICE3:7; end; hence thesis by A3; end; end; definition let C be FormalContext; func C.: -> strict non quasi-empty ContextStr equals ContextStr(#the carrier' of C, the carrier of C, (the Information of C)~ #); coherence by CONLAT_1:def 1; end; theorem for C being strict FormalContext holds (C.:).: = C; theorem Th18: for C being FormalContext for O being Subset of the carrier of C holds (ObjectDerivation(C)).O = (AttributeDerivation(C.:)).O proof let C be FormalContext; let O be Subset of the carrier of C; reconsider O9 = O as Subset of(the carrier' of C.:); set A1 = {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a }; set A2 = {a where a is Object of C.: : for o being Attribute of C.: st o in O9 holds a is-connected-with o }; A1: A1 c= A2 proof let u be set; assume u in A1; then consider a being Attribute of C such that A2: a = u and A3: for o being Object of C st o in O holds o is-connected-with a; reconsider u9 = u as Object of C.: by A2; for o9 being Attribute of C.: st o9 in O9 holds u9 is-connected-with o9 proof let o9 be Attribute of C.:; reconsider o = o9 as Object of C; assume o9 in O9; then o is-connected-with a by A3; then [o,a] in the Information of C by CONLAT_1:def 2; then [a,o] in the Information of C.: by RELAT_1:def 7; hence thesis by A2,CONLAT_1:def 2; end; hence thesis; end; A4: A2 c= A1 proof let u be set; assume u in A2; then consider a being Object of C.: such that A5: a = u and A6: for o being Attribute of C.: st o in O9 holds a is-connected-with o; reconsider u9 = u as Attribute of C by A5; for o being Object of C st o in O holds o is-connected-with u9 proof let o9 be Object of C; reconsider o = o9 as Attribute of C.:; assume o9 in O; then a is-connected-with o by A6; then [a,o] in the Information of C.: by CONLAT_1:def 2; then [o9,u9] in the Information of C by A5,RELAT_1:def 7; hence thesis by CONLAT_1:def 2; end; hence thesis; end; (ObjectDerivation(C)).O = {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } & (AttributeDerivation(C.:) ).O9 = {a where a is Object of C.: : for o being Attribute of C.: st o in O9 holds a is-connected-with o } by CONLAT_1:def 3,def 4; hence thesis by A1,A4,XBOOLE_0:def 10; end; theorem Th19: for C being FormalContext for A being Subset of the carrier' of C holds (AttributeDerivation(C)).A = (ObjectDerivation(C.:)).A proof let C be FormalContext; let O be Subset of the carrier' of C; reconsider O9 = O as Subset of(the carrier of C.:); set A1 = {a where a is Object of C : for o being Attribute of C st o in O holds a is-connected-with o }; set A2 = {a where a is Attribute of C.: : for o being Object of C.: st o in O9 holds o is-connected-with a }; A1: A1 c= A2 proof let u be set; assume u in A1; then consider a being Object of C such that A2: a = u and A3: for o being Attribute of C st o in O holds a is-connected-with o; reconsider u9 = u as Attribute of C.: by A2; for o being Object of C.: st o in O9 holds o is-connected-with u9 proof let o9 be Object of C.:; reconsider o = o9 as Attribute of C; assume o9 in O9; then a is-connected-with o by A3; then [a,o] in the Information of C by CONLAT_1:def 2; then [o9,u9] in the Information of C.: by A2,RELAT_1:def 7; hence thesis by CONLAT_1:def 2; end; hence thesis; end; A4: A2 c= A1 proof let u be set; assume u in A2; then consider a being Attribute of C.: such that A5: a = u and A6: for o being Object of C.: st o in O9 holds o is-connected-with a; reconsider u9 = u as Object of C by A5; for o being Attribute of C st o in O holds u9 is-connected-with o proof let o9 be Attribute of C; reconsider o = o9 as Object of C.:; assume o9 in O; then o is-connected-with a by A6; then [o,a] in the Information of C.: by CONLAT_1:def 2; then [u9,o9] in the Information of C by A5,RELAT_1:def 7; hence thesis by CONLAT_1:def 2; end; hence thesis; end; (AttributeDerivation(C)).O = {a where a is Object of C : for o being Attribute of C st o in O holds a is-connected-with o } & (ObjectDerivation(C.: )).O9 = {a where a is Attribute of C.: : for o being Object of C.: st o in O9 holds o is-connected-with a } by CONLAT_1:def 3,def 4; hence thesis by A1,A4,XBOOLE_0:def 10; end; definition let C be FormalContext; let CP be ConceptStr over C; func CP.: -> strict ConceptStr over C.: means :Def8: the Extent of it = the Intent of CP & the Intent of it = the Extent of CP; existence proof reconsider O = the Intent of CP as Subset of the carrier of C.:; reconsider A = the Extent of CP as Subset of the carrier' of C.:; take ConceptStr(# O,A#); thus thesis; end; uniqueness; end; registration let C be FormalContext; let CP be FormalConcept of C; cluster CP.: -> non empty concept-like; coherence proof reconsider O = the Intent of CP as Subset of the carrier of C.:; reconsider A = the Extent of CP as Subset of the carrier' of C.:; set CPD = ConceptStr(# O,A#); A1: (AttributeDerivation(C.:)).(the Intent of CPD) = (ObjectDerivation(C)) .(the Extent of CP) by Th18 .= the Extent of CPD by CONLAT_1:def 10; A2: CPD = CP.: by Def8; (ObjectDerivation(C.:)).(the Extent of CPD) = (AttributeDerivation(C)) .(the Intent of CP) by Th19 .= the Intent of CPD by CONLAT_1:def 10; hence thesis by A1,A2,Lm3,CONLAT_1:def 10; end; end; theorem for C being strict FormalContext for CP being strict FormalConcept of C holds (CP.:).: = CP proof let C be strict FormalContext; let CP be strict FormalConcept of C; A1: the Intent of (CP.:).: = the Extent of CP.: by Def8 .= the Intent of CP by Def8; the Extent of (CP.:).: = the Intent of CP.: by Def8 .= the Extent of CP by Def8; hence thesis by A1; end; definition let C be FormalContext; func DualHomomorphism(C) -> Homomorphism of (ConceptLattice(C)).:, ConceptLattice(C.:) means :Def9: for CP being strict FormalConcept of C holds it.CP = CP.:; existence proof set f = {[ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] where O is Subset of the carrier of C, A is Subset of the carrier' of C : ConceptStr(#O,A#) is FormalConcept of C }; A1: ConceptLattice(C.:) = LattStr(#B-carrier(C.:),B-join(C.:),B-meet(C.:) #) by CONLAT_1:def 20; A2: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by CONLAT_1:def 20; then A3: (ConceptLattice(C)).: = LattStr(#B-carrier(C),B-meet(C),B-join(C)#) by LATTICE2:def 2; f c= [: the carrier of (ConceptLattice(C)).:, the carrier of ConceptLattice(C.:) :] proof let y be set; assume y in f; then consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A4: y = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] and A5: ConceptStr(#O,A#) is FormalConcept of C; (ConceptStr(#O,A#)).: is strict FormalConcept of C.: by A5; then A6: (ConceptStr(#O,A#)).: in the carrier of ConceptLattice(C.:) by A1, CONLAT_1:31; ConceptStr(#O,A#) in the carrier of (ConceptLattice(C)).: by A3,A5, CONLAT_1:31; hence thesis by A4,A6,ZFMISC_1:def 2; end; then reconsider f as Relation of the carrier of (ConceptLattice(C)).:, the carrier of ConceptLattice(C.:); the carrier of (ConceptLattice(C)).: c= dom f proof let y be set; assume y in the carrier of (ConceptLattice(C)).:; then A7: y is strict FormalConcept of C by A3,CONLAT_1:31; then consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that A8: y = ConceptStr(#O9,A9#); set z = (ConceptStr(#O9,A9#)).:; (ConceptStr(#O9,A9#)).: is strict FormalConcept of C.: by A7,A8; then reconsider z as Element of ConceptLattice(C.:) by A1,CONLAT_1:31; [y,z] in f by A7,A8; hence thesis by XTUPLE_0:def 12; end; then A9: the carrier of (ConceptLattice(C)).: = dom f by XBOOLE_0:def 10; for x,y1,y2 being set st [x,y1] in f & [x,y2] in f holds y1 = y2 proof let x,y1,y2 be set; assume that A10: [x,y1] in f and A11: [x,y2] in f; consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that A12: [x,y2] = [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:] and ConceptStr(#O9,A9#) is FormalConcept of C by A11; consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A13: [x,y1] = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] and ConceptStr(#O,A#) is FormalConcept of C by A10; A14: ConceptStr(#O,A#) = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:]`1 .= [x,y1]`1 by A13 .= x .= [x,y2]`1 .= [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:]`1 by A12 .= ConceptStr(#O9,A9#); thus y1 = [x,y1]`2 .= [x,y2]`2 by A13,A12,A14 .= y2; end; then reconsider f as Function of the carrier of (ConceptLattice(C)).:, the carrier of ConceptLattice(C.:) by A9,FUNCT_1:def 1,FUNCT_2:def 1; A15: (ConceptLattice(C)).: = LattStr(#the carrier of ConceptLattice(C), the L_meet of ConceptLattice(C), the L_join of ConceptLattice(C)#) by LATTICE2:def 2; A16: for a,b being Element of (ConceptLattice(C)).: holds a [= b implies f .a [= f.b proof let a,b be Element of (ConceptLattice(C)).:; reconsider aa = a%, bb = b% as Element of LattPOSet ConceptLattice(C) by A15; reconsider a9 = a, b9 = b as Element of ConceptLattice(C) by A15; A17: dom f = the carrier of (ConceptLattice(C)).: by FUNCT_2:def 1; then consider fa being set such that A18: [a,fa] in f by XTUPLE_0:def 12; assume a [= b; then a% <= b% by LATTICE3:7; then [a%,b%] in the InternalRel of (LattPOSet((ConceptLattice(C)).:)) by ORDERS_2:def 5; then [a%,b%] in (the InternalRel of (LattPOSet (ConceptLattice(C))))~ by LATTICE3:20; then [b%,a%] in the InternalRel of (LattPOSet (ConceptLattice(C))) by RELAT_1:def 7; then A19: bb <= aa by ORDERS_2:def 5; (%aa)% = aa & (%bb)% = bb; then %bb [= %aa by A19,LATTICE3:7; then A20: (%bb)@ is-SubConcept-of (%aa)@ by CONLAT_1:43; consider fb being set such that A21: [b,fb] in f by A17,XTUPLE_0:def 12; A22: fb in rng f by A21,XTUPLE_0:def 13; A23: f.b = fb by A21,FUNCT_1:1; consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that A24: [b,fb] = [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:] and ConceptStr(#O9,A9#) is FormalConcept of C by A21; A25: b = [b,fb]`1 .= [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:]`1 by A24 .= (ConceptStr(#O9,A9#)); A26: fa in rng f by A18,XTUPLE_0:def 13; A27: f.a = fa by A18,FUNCT_1:1; consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A28: [a,fa] = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] and ConceptStr(#O,A#) is FormalConcept of C by A18; reconsider fa as Element of ConceptLattice(C.:) by A26; A29: a = [a,fa]`1 .= [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:]`1 by A28 .= (ConceptStr(#O,A#)); reconsider fb as Element of ConceptLattice(C.:) by A22; fb = [b,fb]`2 .= [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:]`2 by A24 .= (ConceptStr(#O9,A9#)).:; then A30: the Intent of fb@ = the Intent of (ConceptStr(#O9,A9#)).: by CONLAT_1:def 21 .= the Extent of ConceptStr(#O9,A9#) by Def8 .= the Extent of (b9)@ by A25,CONLAT_1:def 21; fa = [a,fa]`2 .= [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:]`2 by A28 .= (ConceptStr(#O,A#)).:; then the Intent of fa@ = the Intent of (ConceptStr(#O,A#)).: by CONLAT_1:def 21 .= the Extent of ConceptStr(#O,A#) by Def8 .= the Extent of (a9)@ by A29,CONLAT_1:def 21; then the Intent of (fb)@ c= the Intent of (fa)@ by A20,A30, CONLAT_1:def 16; then (fa)@ is-SubConcept-of (fb)@ by CONLAT_1:28; hence thesis by A27,A23,CONLAT_1:43; end; the carrier of ConceptLattice(C.:) c= rng f proof let u be set; A31: dom f = the carrier of (ConceptLattice(C)).: by FUNCT_2:def 1; assume u in the carrier of ConceptLattice(C.:); then reconsider u as Element of ConceptLattice(C.:); reconsider A9 = the Intent of u@ as Subset of the carrier of C; reconsider O9 = the Extent of u@ as Subset of the carrier' of C; set CP = ConceptStr(#A9,O9#); A32: not(the Extent of u@ is empty & the Intent of u@ is empty) by CONLAT_1:def 8; A33: (AttributeDerivation(C)).(the Intent of CP) = (ObjectDerivation(C.: )).(the Extent of u@) by Th19 .= the Extent of CP by CONLAT_1:def 10; (ObjectDerivation(C)).(the Extent of CP) = (AttributeDerivation(C.: )).(the Intent of u@) by Th18 .= the Intent of CP by CONLAT_1:def 10; then CP is FormalConcept of C by A33,A32,CONLAT_1:def 8,def 10; then CP in dom f by A15,A2,A31,CONLAT_1:31; then consider v being set such that A34: [CP,v] in f by XTUPLE_0:def 12; consider Ov being Subset of the carrier of C, Av being Subset of the carrier' of C such that A35: [CP,v] = [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).:] and ConceptStr(#Ov,Av#) is FormalConcept of C by A34; A36: CP = [CP,v]`1 .= [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).: ]`1 by A35 .= ConceptStr(#Ov,Av#); A37: v in rng f by A34,XTUPLE_0:def 13; then reconsider v as strict FormalConcept of C.: by A1,CONLAT_1:31; v = [CP,v]`2 .= [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).: ]`2 by A35 .= (ConceptStr(#Ov,Av#)).:; then the Extent of v = the Extent of u@ & the Intent of v = the Intent of u@ by A36,Def8; hence thesis by A37,CONLAT_1:def 21; end; then A38: rng f = the carrier of ConceptLattice(C.:) by XBOOLE_0:def 10; A39: f is one-to-one proof let a,b be set; assume that A40: a in dom f and A41: b in dom f and A42: f.a = f.b; reconsider a,b as Element of (ConceptLattice(C)).: by A40,A41; consider fa being set such that A43: [a,fa] in f by A40,XTUPLE_0:def 12; consider fb being set such that A44: [b,fb] in f by A41,XTUPLE_0:def 12; A45: f.b = fb by A44,FUNCT_1:1; consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A46: [a,fa] = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] and ConceptStr(#O,A#) is FormalConcept of C by A43; A47: a = (ConceptStr(#O,A#)) by A46,XTUPLE_0:1; consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that A48: [b,fb] = [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:] and ConceptStr(#O9,A9#) is FormalConcept of C by A44; A49: b = (ConceptStr(#O9,A9#)) by A48,XTUPLE_0:1; A50: (ConceptStr(#O9,A9#)).: = fb by A48,XTUPLE_0:1 .= fa by A42,A43,A45,FUNCT_1:1 .= (ConceptStr(#O,A#)).: by A46,XTUPLE_0:1; then A51: the Intent of ConceptStr(#O9,A9#) = the Extent of (ConceptStr(#O,A #)).: by Def8 .= the Intent of ConceptStr(#O,A#) by Def8; the Extent of ConceptStr(#O9,A9#) = the Intent of (ConceptStr(#O,A #)).: by A50,Def8 .= the Extent of ConceptStr(#O,A#) by Def8; hence thesis by A47,A49,A51; end; for a,b being Element of (ConceptLattice(C)).: holds f.a [= f.b implies a [= b proof let a,b be Element of (ConceptLattice(C)).:; A52: dom f = the carrier of (ConceptLattice(C)).: by FUNCT_2:def 1; then consider fa being set such that A53: [a,fa] in f by XTUPLE_0:def 12; reconsider a9 = a, b9 = b as Element of ConceptLattice(C) by A15; assume f.a [= f.b; then A54: (f.a)@ is-SubConcept-of (f.b)@ by CONLAT_1:43; consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A55: [a,fa] = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] and ConceptStr(#O,A#) is FormalConcept of C by A53; A56: a = (ConceptStr(#O,A#)) by A55,XTUPLE_0:1; A57: fa in rng f by A53,XTUPLE_0:def 13; consider fb being set such that A58: [b,fb] in f by A52,XTUPLE_0:def 12; A59: fb in rng f by A58,XTUPLE_0:def 13; consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that A60: [b,fb] = [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:] and ConceptStr(#O9,A9#) is FormalConcept of C by A58; A61: b = (ConceptStr(#O9,A9#)) by A60,XTUPLE_0:1; reconsider fb as Element of ConceptLattice(C.:) by A59; A62: fb = (ConceptStr(#O9,A9#)).: by A60,XTUPLE_0:1; A63: the Intent of (f.b)@ = the Intent of fb@ by A58,FUNCT_1:1 .= the Intent of (ConceptStr(#O9,A9#)).: by A62,CONLAT_1:def 21 .= the Extent of ConceptStr(#O9,A9#) by Def8 .= the Extent of (b9)@ by A61,CONLAT_1:def 21; reconsider fa as Element of ConceptLattice(C.:) by A57; A64: fa = (ConceptStr(#O,A#)).: by A55,XTUPLE_0:1; the Intent of (f.a)@ = the Intent of fa@ by A53,FUNCT_1:1 .= the Intent of (ConceptStr(#O,A#)).: by A64,CONLAT_1:def 21 .= the Extent of ConceptStr(#O,A#) by Def8 .= the Extent of (a9)@ by A56,CONLAT_1:def 21; then the Extent of (b9)@ c= the Extent of (a9)@ by A54,A63,CONLAT_1:28; then (b9)@ is-SubConcept-of (a9)@ by CONLAT_1:def 16; then b9 [= a9 by CONLAT_1:43; then (b9)% <= (a9)% by LATTICE3:7; then [(b9)%,(a9)%] in the InternalRel of (LattPOSet(ConceptLattice(C)) ) by ORDERS_2:def 5; then [a%,b%] in the InternalRel of (LattPOSet (ConceptLattice(C)))~ by RELAT_1:def 7; then [a%,b%] in the InternalRel of (LattPOSet (ConceptLattice(C)).:) by LATTICE3:20; then a% <= b% by ORDERS_2:def 5; hence thesis by LATTICE3:7; end; then reconsider f as Homomorphism of (ConceptLattice(C)).:,ConceptLattice(C.:) by A16,A38,A39,Lm2; for CP being strict FormalConcept of C holds f.CP = CP.: proof let CP be strict FormalConcept of C; CP in B-carrier(C) by CONLAT_1:31; then CP in dom f by A3,FUNCT_2:def 1; then consider v being set such that A65: [CP,v] in f by XTUPLE_0:def 12; A66: v in rng f by A65,XTUPLE_0:def 13; consider Ov being Subset of the carrier of C, Av being Subset of the carrier' of C such that A67: [CP,v] = [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).:] and ConceptStr(#Ov,Av#) is FormalConcept of C by A65; reconsider v as strict FormalConcept of C.: by A1,A66,CONLAT_1:31; A68: CP = ConceptStr(#Ov,Av#) by A67,XTUPLE_0:1; v = (ConceptStr(#Ov,Av#)).: by A67,XTUPLE_0:1; hence thesis by A65,A68,FUNCT_1:1; end; hence thesis; end; uniqueness proof let F1,F2 be Homomorphism of (ConceptLattice(C)).:,ConceptLattice(C.:); assume A69: for CP being strict FormalConcept of C holds F1.CP = CP.:; assume A70: for CP being strict FormalConcept of C holds F2.CP = CP.:; A71: for u being set st u in the carrier of (ConceptLattice(C)).: holds F1.u = F2.u proof let u be set; ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by CONLAT_1:def 20; then A72: (ConceptLattice(C)).: = LattStr(#B-carrier(C),B-meet(C),B-join(C) #) by LATTICE2:def 2; assume u in the carrier of (ConceptLattice(C)).:; then reconsider u as strict FormalConcept of C by A72,CONLAT_1:31; F1.u = u.: by A69 .= F2.u by A70; hence thesis; end; dom F1 = the carrier of (ConceptLattice(C)).: & dom F2 = the carrier of ( ConceptLattice(C)).: by FUNCT_2:def 1; hence thesis by A71,FUNCT_1:2; end; end; theorem Th21: for C being FormalContext holds DualHomomorphism(C) is bijective proof let C be FormalContext; set f = DualHomomorphism(C); A1: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by CONLAT_1:def 20; A2: (ConceptLattice(C)).: = LattStr(#the carrier of ConceptLattice(C), the L_meet of ConceptLattice(C), the L_join of ConceptLattice(C)#) by LATTICE2:def 2; the carrier of ConceptLattice(C.:) c= rng f proof let u be set; assume u in the carrier of ConceptLattice(C.:); then reconsider u as Element of ConceptLattice(C.:); reconsider A9 = the Intent of u@ as Subset of the carrier of C; reconsider O9 = the Extent of u@ as Subset of the carrier' of C; set CP = ConceptStr(#A9,O9#); A3: not(the Extent of u@ is empty & the Intent of u@ is empty) by CONLAT_1:def 8; A4: (AttributeDerivation(C)).(the Intent of CP) = (ObjectDerivation(C.:)) .(the Extent of u@) by Th19 .= the Extent of CP by CONLAT_1:def 10; A5: (ObjectDerivation(C)).(the Extent of CP) = (AttributeDerivation(C.:)) .(the Intent of u@) by Th18 .= the Intent of CP by CONLAT_1:def 10; then CP is FormalConcept of C by A4,A3,CONLAT_1:def 8,def 10; then A6: CP in the carrier of (ConceptLattice(C)) by A1,CONLAT_1:31; reconsider CP as strict FormalConcept of C by A5,A4,A3,CONLAT_1:def 8 ,def 10; A7: the Extent of CP.: = the Extent of u@ by Def8; f.CP = CP.: & the Intent of CP.: = the Intent of u@ by Def8,Def9; then A8: f.CP = u by A7,CONLAT_1:def 21; CP in dom f by A2,A6,FUNCT_2:def 1; hence thesis by A8,FUNCT_1:def 3; end; then rng f = the carrier of ConceptLattice(C.:) by XBOOLE_0:def 10; then A9: f is onto by FUNCT_2:def 3; f is one-to-one proof let a,b be set; assume that A10: a in dom f & b in dom f and A11: f.a = f.b; reconsider a,b as Element of (ConceptLattice(C)).: by A10; (ConceptLattice(C)).: = LattStr(#the carrier of ConceptLattice(C), the L_meet of ConceptLattice(C), the L_join of ConceptLattice(C)#) by LATTICE2:def 2; then reconsider a,b as Element of ConceptLattice(C); A12: f.(a@) = f.a & f.(b@) = f.b by CONLAT_1:def 21; A13: f.(a@) = (a@).: & f.(b@) = (b@).: by Def9; then A14: the Extent of a@ = the Intent of (b@).: by A11,A12,Def8 .= the Extent of b@ by Def8; the Intent of a@ = the Extent of (b@).: by A11,A13,A12,Def8 .= the Intent of b@ by Def8; then a = b@ by A14,CONLAT_1:def 21 .= b by CONLAT_1:def 21; hence thesis; end; hence thesis by A9; end; theorem for C being FormalContext holds ConceptLattice(C.:),(ConceptLattice(C) ).: are_isomorphic proof let C be FormalContext; DualHomomorphism(C) is bijective by Th21; hence thesis by LATTICE4:def 2; end;