:: CONLAT_2 semantic presentation begin definition let C be FormalContext; let CP be strict FormalConcept of C; func @ CP -> Element of (ConceptLattice C) equals :: CONLAT_2:def 1 CP; coherence CP is Element of (ConceptLattice C) proof ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def_20; hence CP is Element of (ConceptLattice C) by CONLAT_1:31; ::_thesis: verum end; end; :: deftheorem defines @ CONLAT_2:def_1_:_ for C being FormalContext for CP being strict FormalConcept of C holds @ CP = CP; registration let C be FormalContext; cluster ConceptLattice C -> bounded ; coherence ConceptLattice C is bounded 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); ::_thesis: a [= @ (Concept-with-all-Objects C) a @ is-SubConcept-of (@ (Concept-with-all-Objects C)) @ by A1, CONLAT_1:30; hence a [= @ (Concept-with-all-Objects C) by CONLAT_1:43; ::_thesis: verum 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); ::_thesis: ( (@ (Concept-with-all-Objects C)) "\/" a = @ (Concept-with-all-Objects C) & a "\/" (@ (Concept-with-all-Objects C)) = @ (Concept-with-all-Objects C) ) a [= @ (Concept-with-all-Objects C) by A2; hence ( (@ (Concept-with-all-Objects C)) "\/" a = @ (Concept-with-all-Objects C) & a "\/" (@ (Concept-with-all-Objects C)) = @ (Concept-with-all-Objects C) ) by LATTICES:def_3; ::_thesis: verum 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); ::_thesis: @ (Concept-with-all-Attributes C) [= a (@ (Concept-with-all-Attributes C)) @ is-SubConcept-of a @ by A4, CONLAT_1:30; hence @ (Concept-with-all-Attributes C) [= a by CONLAT_1:43; ::_thesis: verum 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); ::_thesis: ( (@ (Concept-with-all-Attributes C)) "/\" a = @ (Concept-with-all-Attributes C) & a "/\" (@ (Concept-with-all-Attributes C)) = @ (Concept-with-all-Attributes C) ) @ (Concept-with-all-Attributes C) [= a by A5; hence ( (@ (Concept-with-all-Attributes C)) "/\" a = @ (Concept-with-all-Attributes C) & a "/\" (@ (Concept-with-all-Attributes C)) = @ (Concept-with-all-Attributes C) ) by LATTICES:4; ::_thesis: verum end; then ConceptLattice C is lower-bounded by LATTICES:def_13; hence ConceptLattice C is bounded by A3; ::_thesis: verum end; end; theorem Th1: :: CONLAT_2:1 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; ::_thesis: ( Bottom (ConceptLattice C) = Concept-with-all-Attributes C & Top (ConceptLattice C) = Concept-with-all-Objects C ) 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); ::_thesis: a [= @ (Concept-with-all-Objects C) a @ is-SubConcept-of (@ (Concept-with-all-Objects C)) @ by A1, CONLAT_1:30; hence a [= @ (Concept-with-all-Objects C) by CONLAT_1:43; ::_thesis: verum 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); ::_thesis: ( (@ (Concept-with-all-Objects C)) "\/" a = @ (Concept-with-all-Objects C) & a "\/" (@ (Concept-with-all-Objects C)) = @ (Concept-with-all-Objects C) ) a [= @ (Concept-with-all-Objects C) by A2; hence ( (@ (Concept-with-all-Objects C)) "\/" a = @ (Concept-with-all-Objects C) & a "\/" (@ (Concept-with-all-Objects C)) = @ (Concept-with-all-Objects C) ) by LATTICES:def_3; ::_thesis: verum 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); ::_thesis: @ (Concept-with-all-Attributes C) [= a (@ (Concept-with-all-Attributes C)) @ is-SubConcept-of a @ by A4, CONLAT_1:30; hence @ (Concept-with-all-Attributes C) [= a by CONLAT_1:43; ::_thesis: verum 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); ::_thesis: ( (@ (Concept-with-all-Attributes C)) "/\" a = @ (Concept-with-all-Attributes C) & a "/\" (@ (Concept-with-all-Attributes C)) = @ (Concept-with-all-Attributes C) ) @ (Concept-with-all-Attributes C) [= a by A5; hence ( (@ (Concept-with-all-Attributes C)) "/\" a = @ (Concept-with-all-Attributes C) & a "/\" (@ (Concept-with-all-Attributes C)) = @ (Concept-with-all-Attributes C) ) by LATTICES:4; ::_thesis: verum end; hence ( Bottom (ConceptLattice C) = Concept-with-all-Attributes C & Top (ConceptLattice C) = Concept-with-all-Objects C ) by A3, LATTICES:def_16, LATTICES:def_17; ::_thesis: verum end; theorem Th2: :: CONLAT_2:2 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; ::_thesis: 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 } let D be non empty Subset-Family of the carrier of C; ::_thesis: (ObjectDerivation C) . (union D) = meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } 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 } ; percases ( { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } <> {} or { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } = {} ) ; supposeA1: { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } <> {} ; ::_thesis: (ObjectDerivation C) . (union D) = meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } thus (ObjectDerivation C) . (union D) c= meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } :: according to XBOOLE_0:def_10 ::_thesis: meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } c= (ObjectDerivation C) . (union D) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (ObjectDerivation C) . (union D) or x in meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } ) assume x in (ObjectDerivation C) . (union D) ; ::_thesis: x in meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } 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 = x as Attribute of C ; A3: for O being Subset of the carrier of C st O in D holds 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; ::_thesis: ( O in D implies for o being Object of C st o in O holds o is-connected-with x ) assume A4: O in D ; ::_thesis: for o being Object of C st o in O holds o is-connected-with x let o be Object of C; ::_thesis: ( o in O implies o is-connected-with x ) assume o in O ; ::_thesis: o is-connected-with x then o in union D by A4, TARSKI:def_4; hence o is-connected-with x by A2; ::_thesis: verum 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; ::_thesis: ( O in D implies x in (ObjectDerivation C) . O ) assume O in D ; ::_thesis: x in (ObjectDerivation C) . O 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 x in (ObjectDerivation C) . O by CONLAT_1:def_3; ::_thesis: verum end; for Y being set st Y in { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } holds x in Y proof let Y be set ; ::_thesis: ( Y in { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } implies x in Y ) assume Y in { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } ; ::_thesis: x in Y then ex O being Subset of the carrier of C st ( Y = (ObjectDerivation C) . O & O in D ) ; hence x in Y by A5; ::_thesis: verum end; hence x in meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } by A1, SETFAM_1:def_1; ::_thesis: verum end; thus meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } c= (ObjectDerivation C) . (union D) ::_thesis: verum 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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } or x in (ObjectDerivation C) . (union D) ) assume A6: x in meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } ; ::_thesis: x in (ObjectDerivation C) . (union D) then A7: x in the Element of { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } by A1, SETFAM_1:def_1; the Element of { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in 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 ( the Element of { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } = (ObjectDerivation C) . X & X in D ) ; then reconsider x = 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; ::_thesis: ( O in D implies x in (ObjectDerivation C) . O ) assume O in D ; ::_thesis: x in (ObjectDerivation C) . O then (ObjectDerivation C) . O in { ((ObjectDerivation C) . O9) where O9 is Subset of the carrier of C : O9 in D } ; hence x in (ObjectDerivation C) . O by A6, SETFAM_1:def_1; ::_thesis: verum end; A9: for O being Subset of the carrier of C st O in D holds 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; ::_thesis: ( O in D implies for o being Object of C st o in O holds o is-connected-with x ) assume O in D ; ::_thesis: for o being Object of C st o in O holds o is-connected-with x 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; ::_thesis: ( o in O implies o is-connected-with x ) assume o in O ; ::_thesis: o is-connected-with x hence o is-connected-with x by A10; ::_thesis: verum 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; ::_thesis: ( o in union D implies o is-connected-with x ) assume o in union D ; ::_thesis: o is-connected-with x then ex Y being set st ( o in Y & Y in D ) by TARSKI:def_4; hence o is-connected-with x by A9; ::_thesis: verum 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 x in (ObjectDerivation C) . (union D) by CONLAT_1:def_3; ::_thesis: verum end; end; supposeA11: { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } = {} ; ::_thesis: (ObjectDerivation C) . (union D) = meet { ((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 <> {} ; ::_thesis: contradiction (ObjectDerivation C) . the Element of D in { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } ; hence contradiction by A11; ::_thesis: verum end; hence (ObjectDerivation C) . (union D) = meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } ; ::_thesis: verum end; end; end; theorem Th3: :: CONLAT_2:3 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; ::_thesis: 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 } let D be non empty Subset-Family of the carrier' of C; ::_thesis: (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } 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__::_thesis:_(_(__{__((AttributeDerivation_C)_._A)_where_A_is_Subset_of_the_carrier'_of_C_:_A_in_D__}__<>_{}_&_(AttributeDerivation_C)_._(union_D)_=_meet__{__((AttributeDerivation_C)_._A)_where_A_is_Subset_of_the_carrier'_of_C_:_A_in_D__}__)_or_(__{__((AttributeDerivation_C)_._A)_where_A_is_Subset_of_the_carrier'_of_C_:_A_in_D__}__=_{}_&_(AttributeDerivation_C)_._(union_D)_=_meet__{__((AttributeDerivation_C)_._A)_where_A_is_Subset_of_the_carrier'_of_C_:_A_in_D__}__)_) percases ( { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } <> {} or { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } = {} ) ; caseA1: { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } <> {} ; ::_thesis: (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } thus (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ::_thesis: verum proof thus (AttributeDerivation C) . (union D) c= meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } :: according to XBOOLE_0:def_10 ::_thesis: meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } c= (AttributeDerivation C) . (union D) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (AttributeDerivation C) . (union D) or x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ) assume x in (AttributeDerivation C) . (union D) ; ::_thesis: x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } 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 = x as Object of C ; A3: for A being Subset of the carrier' of C st A in D holds 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; ::_thesis: ( A in D implies for a being Attribute of C st a in A holds x is-connected-with a ) assume A4: A in D ; ::_thesis: for a being Attribute of C st a in A holds x is-connected-with a let a be Attribute of C; ::_thesis: ( a in A implies x is-connected-with a ) assume a in A ; ::_thesis: x is-connected-with a then a in union D by A4, TARSKI:def_4; hence x is-connected-with a by A2; ::_thesis: verum 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; ::_thesis: ( A in D implies x in (AttributeDerivation C) . A ) assume A in D ; ::_thesis: x in (AttributeDerivation C) . A 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 x in (AttributeDerivation C) . A by CONLAT_1:def_4; ::_thesis: verum end; for Y being set st Y in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } holds x in Y proof let Y be set ; ::_thesis: ( Y in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } implies x in Y ) assume Y in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; ::_thesis: x in Y then ex A being Subset of the carrier' of C st ( Y = (AttributeDerivation C) . A & A in D ) ; hence x in Y by A5; ::_thesis: verum end; hence x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } by A1, SETFAM_1:def_1; ::_thesis: verum 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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } or x in (AttributeDerivation C) . (union D) ) assume A6: x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; ::_thesis: x in (AttributeDerivation C) . (union D) then A7: x in the Element of { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } by A1, SETFAM_1:def_1; the Element of { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in 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 ( the Element of { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } = (AttributeDerivation C) . X & X in D ) ; then reconsider x = 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; ::_thesis: ( A in D implies x in (AttributeDerivation C) . A ) assume A in D ; ::_thesis: x in (AttributeDerivation C) . A then (AttributeDerivation C) . A in { ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in D } ; hence x in (AttributeDerivation C) . A by A6, SETFAM_1:def_1; ::_thesis: verum end; A9: for A being Subset of the carrier' of C st A in D holds 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; ::_thesis: ( A in D implies for a being Attribute of C st a in A holds x is-connected-with a ) assume A in D ; ::_thesis: for a being Attribute of C st a in A holds x is-connected-with a 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; ::_thesis: ( a in A implies x is-connected-with a ) assume a in A ; ::_thesis: x is-connected-with a hence x is-connected-with a by A10; ::_thesis: verum 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; ::_thesis: ( a in union D implies x is-connected-with a ) assume a in union D ; ::_thesis: x is-connected-with a then ex Y being set st ( a in Y & Y in D ) by TARSKI:def_4; hence x is-connected-with a by A9; ::_thesis: verum 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 x in (AttributeDerivation C) . (union D) by CONLAT_1:def_4; ::_thesis: verum end; end; caseA11: { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } = {} ; ::_thesis: (AttributeDerivation C) . (union D) = meet { ((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 <> {} ; ::_thesis: contradiction (AttributeDerivation C) . the Element of D in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; hence contradiction by A11; ::_thesis: verum end; hence (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; ::_thesis: verum end; end; end; hence (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; ::_thesis: verum end; theorem Th4: :: CONLAT_2:4 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; ::_thesis: for D being Subset of (ConceptLattice C) holds ( "/\" (D,(ConceptLattice C)) is FormalConcept of C & "\/" (D,(ConceptLattice C)) is FormalConcept of C ) let D be Subset of (ConceptLattice C); ::_thesis: ( "/\" (D,(ConceptLattice C)) is FormalConcept of C & "\/" (D,(ConceptLattice C)) is FormalConcept of C ) ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def_20; hence ( "/\" (D,(ConceptLattice C)) is FormalConcept of C & "\/" (D,(ConceptLattice C)) is FormalConcept of C ) by CONLAT_1:31; ::_thesis: verum end; definition let C be FormalContext; let D be Subset of (ConceptLattice C); func "/\" (D,C) -> FormalConcept of C equals :: CONLAT_2:def 2 "/\" (D,(ConceptLattice C)); coherence "/\" (D,(ConceptLattice C)) is FormalConcept of C by Th4; func "\/" (D,C) -> FormalConcept of C equals :: CONLAT_2:def 3 "\/" (D,(ConceptLattice C)); coherence "\/" (D,(ConceptLattice C)) is FormalConcept of C by Th4; end; :: deftheorem defines "/\" CONLAT_2:def_2_:_ for C being FormalContext for D being Subset of (ConceptLattice C) holds "/\" (D,C) = "/\" (D,(ConceptLattice C)); :: deftheorem defines "\/" CONLAT_2:def_3_:_ for C being FormalContext for D being Subset of (ConceptLattice C) holds "\/" (D,C) = "\/" (D,(ConceptLattice C)); theorem :: CONLAT_2:5 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; ::_thesis: ( "\/" (({} (ConceptLattice C)),C) = Concept-with-all-Attributes C & "/\" (({} (ConceptLattice C)),C) = Concept-with-all-Objects C ) 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); ::_thesis: ( b is_less_than {} implies b [= @ (Concept-with-all-Objects C) ) assume b is_less_than {} ; ::_thesis: b [= @ (Concept-with-all-Objects C) ( b @ is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Objects C = (@ (Concept-with-all-Objects C)) @ ) by CONLAT_1:30, CONLAT_1:def_21; hence b [= @ (Concept-with-all-Objects C) by CONLAT_1:43; ::_thesis: verum 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, LATTICE3:def_16; hence ( "\/" (({} (ConceptLattice C)),C) = Concept-with-all-Attributes C & "/\" (({} (ConceptLattice C)),C) = Concept-with-all-Objects C ) by A1, Th1, LATTICE3:34; ::_thesis: verum end; theorem :: CONLAT_2:6 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; ::_thesis: ( "\/" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Objects C & "/\" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Attributes C ) A1: @ (Concept-with-all-Attributes C) is_less_than [#] the carrier of (ConceptLattice C) proof let q be Element of (ConceptLattice C); :: according to LATTICE3:def_16 ::_thesis: ( not q in [#] the carrier of (ConceptLattice C) or @ (Concept-with-all-Attributes C) [= q ) assume q in [#] the carrier of (ConceptLattice C) ; ::_thesis: @ (Concept-with-all-Attributes C) [= q ( Concept-with-all-Attributes C is-SubConcept-of q @ & Concept-with-all-Attributes C = (@ (Concept-with-all-Attributes C)) @ ) by CONLAT_1:30, CONLAT_1:def_21; hence @ (Concept-with-all-Attributes C) [= q by CONLAT_1:43; ::_thesis: verum 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, LATTICE3:def_16; hence ( "\/" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Objects C & "/\" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Attributes C ) by A1, Th1, LATTICE3:34; ::_thesis: verum end; theorem :: CONLAT_2:7 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; ::_thesis: 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 } ) let D be non empty Subset of (ConceptLattice C); ::_thesis: ( 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 } ) 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 ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in bool the carrier of C ) 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 } ; ::_thesis: x in bool the carrier of C then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st ( x = the Extent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) ; hence x in bool the carrier of C ; ::_thesis: verum 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 ; (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 } )) 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 } ; 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 ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in the carrier of C ) 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 } ; ::_thesis: x in the carrier of C 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 ex I being Subset of the carrier' of C st ( Y = the Extent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A2; hence x in the carrier of C by A1; ::_thesis: verum end; then reconsider 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 } as Subset of the carrier of C ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (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 } )) or x in the carrier of C ) A3: (AttributeDerivation C) . ((ObjectDerivation C) . u) is Element of bool the carrier of C ; assume x in (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 } )) ; ::_thesis: x in the carrier of C hence x in the carrier of C by A3; ::_thesis: verum end; then reconsider 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 } )) 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 st x in D holds ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) proof let x be set ; ::_thesis: ( x in D implies ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) ) assume x in D ; ::_thesis: ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) then x is strict FormalConcept of C by A4, CONLAT_1:31; hence ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) ; ::_thesis: verum end; then ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) ; then the Extent of the Element of D 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 = 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 ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or 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 } } ) 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 } ; ::_thesis: 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 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 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 } } by A9; ::_thesis: verum 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 ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } } or 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 } ) 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 } } ; ::_thesis: 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 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 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 } by A13; ::_thesis: verum 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: (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 } ) = meet { ((ObjectDerivation C) . O9) where O9 is Subset of the carrier of C : O9 in OO } by Th2; (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 } ) 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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in (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 } ) or x in the carrier' of C ) ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) by A5; then A16: the Intent of the Element of D 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 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 } 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 ex I1 being Subset of the carrier' of C st ( 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 } = the Intent of ConceptStr(# E1,I1 #) & ConceptStr(# E1,I1 #) in D ) ; assume x in (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 } ) ; ::_thesis: x in the carrier' of C then x in 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 } by A15, A14, A16, SETFAM_1:def_1; hence x in the carrier' of C by A17; ::_thesis: verum end; then reconsider a = (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 } ) 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 ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in the carrier of C ) 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 } ; ::_thesis: x in the carrier of C 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 ex I being Subset of the carrier' of C st ( Y = the Extent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A19; hence x in the carrier of C by A18; ::_thesis: verum 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); ::_thesis: ( D is_less_than r implies CP [= r ) assume A22: D is_less_than r ; ::_thesis: CP [= 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); ::_thesis: ( q in D implies the Intent of (r @) c= the Intent of (q @) ) assume q in D ; ::_thesis: the Intent of (r @) c= the Intent of (q @) then q [= r by A22, LATTICE3:def_17; then q @ is-SubConcept-of r @ by CONLAT_1:43; hence the Intent of (r @) c= the Intent of (q @) by CONLAT_1:28; ::_thesis: verum 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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Intent of (r @) or x in 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 } ) assume A24: x in the Intent of (r @) ; ::_thesis: x in 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 } A25: for Y being set st 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 } holds x in Y proof let Y be set ; ::_thesis: ( 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 ) 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 } ; ::_thesis: x in Y 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 x in Y by A26, CONLAT_1:def_21; ::_thesis: verum end; ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) by A5; then the Intent of the Element of D 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 x in 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 A25, SETFAM_1:def_1; ::_thesis: verum end; then CP @ is-SubConcept-of r @ by A20, CONLAT_1:28; hence CP [= r by CONLAT_1:43; ::_thesis: verum end; D is_less_than CP proof let q be Element of (ConceptLattice C); :: according to LATTICE3:def_17 ::_thesis: ( not q in D or q [= CP ) assume q in D ; ::_thesis: q [= CP 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 q [= CP by CONLAT_1:43; ::_thesis: verum end; hence ( 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 } ) by A15, A14, A21, LATTICE3:def_21; ::_thesis: verum end; theorem :: CONLAT_2:8 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; ::_thesis: 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 } )) ) let D be non empty Subset of (ConceptLattice C); ::_thesis: ( 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 } )) ) 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 ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in bool the carrier' of C ) 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 } ; ::_thesis: x in bool the carrier' of C then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st ( x = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) ; hence x in bool the carrier' of C ; ::_thesis: verum 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 ; (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 } )) 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 } ; 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 ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in the carrier' of C ) 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 } ; ::_thesis: x in the carrier' of C 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 ex I being Subset of the carrier' of C st ( Y = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A2; hence x in the carrier' of C by A1; ::_thesis: verum end; then reconsider 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 } as Subset of the carrier' of C ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (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 } )) or x in the carrier' of C ) A3: (ObjectDerivation C) . ((AttributeDerivation C) . u) is Element of bool the carrier' of C ; assume x in (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 } )) ; ::_thesis: x in the carrier' of C hence x in the carrier' of C by A3; ::_thesis: verum end; then reconsider 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 } )) 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 st x in D holds ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) proof let x be set ; ::_thesis: ( x in D implies ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) ) assume x in D ; ::_thesis: ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) then x is strict FormalConcept of C by A4, CONLAT_1:31; hence ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) ; ::_thesis: verum end; then ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) ; then the Intent of the Element of D 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 = 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 ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or 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 } } ) 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 } ; ::_thesis: 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 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 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 } } by A9; ::_thesis: verum 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 ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } } or 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 } ) 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 } } ; ::_thesis: 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 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 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 } by A13; ::_thesis: verum 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: (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 } ) = meet { ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in AA } by Th3; (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 } ) 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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in (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 } ) or x in the carrier of C ) ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) by A5; then A16: the Extent of the Element of D 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 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 } 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 ex I1 being Subset of the carrier' of C st ( 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 } = the Extent of ConceptStr(# E1,I1 #) & ConceptStr(# E1,I1 #) in D ) ; assume x in (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 } ) ; ::_thesis: x in the carrier of C then x in 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 } by A15, A14, A16, SETFAM_1:def_1; hence x in the carrier of C by A17; ::_thesis: verum end; then reconsider o = (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 } ) 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 ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in the carrier' of C ) 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 } ; ::_thesis: x in the carrier' of C 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 ex I being Subset of the carrier' of C st ( Y = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A19; hence x in the carrier' of C by A18; ::_thesis: verum 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); ::_thesis: ( r is_less_than D implies r [= CP ) assume A22: r is_less_than D ; ::_thesis: r [= CP 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); ::_thesis: ( q in D implies the Extent of (r @) c= the Extent of (q @) ) assume q in D ; ::_thesis: the Extent of (r @) c= the Extent of (q @) then r [= q by A22, LATTICE3:def_16; then r @ is-SubConcept-of q @ by CONLAT_1:43; hence the Extent of (r @) c= the Extent of (q @) by CONLAT_1:def_16; ::_thesis: verum 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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Extent of (r @) or x in 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 } ) assume A24: x in the Extent of (r @) ; ::_thesis: x in 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 } A25: for Y being set st 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 } holds x in Y proof let Y be set ; ::_thesis: ( 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 ) 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 } ; ::_thesis: x in Y 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 x in Y by A26, CONLAT_1:def_21; ::_thesis: verum end; ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) by A5; then the Extent of the Element of D 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 x in 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 A25, SETFAM_1:def_1; ::_thesis: verum end; then r @ is-SubConcept-of CP @ by A20, CONLAT_1:def_16; hence r [= CP by CONLAT_1:43; ::_thesis: verum end; CP is_less_than D proof let q be Element of (ConceptLattice C); :: according to LATTICE3:def_16 ::_thesis: ( not q in D or CP [= q ) assume q in D ; ::_thesis: CP [= q 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 CP [= q by CONLAT_1:43; ::_thesis: verum end; hence ( 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 } )) ) by A15, A14, A21, LATTICE3:34; ::_thesis: verum end; theorem Th9: :: CONLAT_2:9 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; ::_thesis: 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 let CP be strict FormalConcept of C; ::_thesis: "\/" ( { 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 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 { 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} ) } is_less_than CP9 holds @ CP [= CP9 proof let CP9 be Element of (ConceptLattice C); ::_thesis: ( { 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} ) } is_less_than CP9 implies @ CP [= CP9 ) assume A2: { 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} ) } is_less_than CP9 ; ::_thesis: @ CP [= CP9 A3: the Extent of CP c= the Extent of (CP9 @) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Extent of CP or x in the Extent of (CP9 @) ) assume A4: x in the Extent of CP ; ::_thesis: x in the Extent of (CP9 @) then reconsider x = x as Element of C ; set Ax = (ObjectDerivation C) . {x}; set Ox = (AttributeDerivation C) . ((ObjectDerivation C) . {x}); reconsider Cx = ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . {x})),((ObjectDerivation C) . {x}) #) 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= (AttributeDerivation C) . ((ObjectDerivation C) . {x}) 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 x in the Extent of (CP9 @) by A6; ::_thesis: verum end; CP = (@ CP) @ by CONLAT_1:def_21; then (@ CP) @ is-SubConcept-of CP9 @ by A3, CONLAT_1:def_16; hence @ CP [= CP9 by CONLAT_1:43; ::_thesis: verum 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 CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } is_less_than @ CP proof let q be Element of (ConceptLattice C); :: according to LATTICE3:def_17 ::_thesis: ( not q 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} ) } or q [= @ CP ) assume q 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} ) } ; ::_thesis: q [= @ CP 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, CONLAT_1: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 q [= @ CP by A12, CONLAT_1:43; ::_thesis: verum end; hence "\/" ( { 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 by A1, LATTICE3:def_21; ::_thesis: verum end; theorem Th10: :: CONLAT_2:10 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; ::_thesis: 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 let CP be strict FormalConcept of C; ::_thesis: "/\" ( { 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 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 { 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}) ) } holds CP9 [= @ CP proof let CP9 be Element of (ConceptLattice C); ::_thesis: ( CP9 is_less_than { 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}) ) } implies CP9 [= @ CP ) assume A2: CP9 is_less_than { 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}) ) } ; ::_thesis: CP9 [= @ CP A3: the Intent of CP c= the Intent of (CP9 @) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Intent of CP or x in the Intent of (CP9 @) ) assume A4: x in the Intent of CP ; ::_thesis: x in the Intent of (CP9 @) then reconsider x = x as Element of the carrier' of C ; set Ax = (ObjectDerivation C) . ((AttributeDerivation C) . {x}); set Ox = (AttributeDerivation C) . {x}; reconsider Cx = ConceptStr(# ((AttributeDerivation C) . {x}),((ObjectDerivation C) . ((AttributeDerivation C) . {x})) #) 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= (ObjectDerivation C) . ((AttributeDerivation C) . {x}) 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 x in the Intent of (CP9 @) by A6; ::_thesis: verum end; CP = (@ CP) @ by CONLAT_1:def_21; then CP9 @ is-SubConcept-of (@ CP) @ by A3, CONLAT_1:28; hence CP9 [= @ CP by CONLAT_1:43; ::_thesis: verum end; @ CP is_less_than { 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}) ) } proof let q be Element of (ConceptLattice C); :: according to LATTICE3:def_16 ::_thesis: ( not q 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}) ) } or @ CP [= q ) assume q 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}) ) } ; ::_thesis: @ CP [= q 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, CONLAT_1: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 @ CP [= q by A12, CONLAT_1:43; ::_thesis: verum end; hence "/\" ( { 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 by A1, LATTICE3:34; ::_thesis: verum end; definition let C be FormalContext; func gamma C -> Function of the carrier of C, the carrier of (ConceptLattice C) means :Def4: :: CONLAT_2:def 4 for o being Element of C ex O being Subset of the carrier of C ex 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 ex b1 being Function of the carrier of C, the carrier of (ConceptLattice C) st for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) proof defpred S1[ set , set ] means ex O being Subset of the carrier of C ex 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 holds ex u being set st ( u in the carrier of (ConceptLattice C) & S1[e,u] ) proof let e be set ; ::_thesis: ( e in the carrier of C implies ex u being set st ( u in the carrier of (ConceptLattice C) & S1[e,u] ) ) assume e in the carrier of C ; ::_thesis: ex u being set st ( u in the carrier of (ConceptLattice C) & S1[e,u] ) 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(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) ; ::_thesis: ( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) in the carrier of (ConceptLattice C) & S1[e, ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #)] ) ( ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) & ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) is FormalConcept of C ) by CONLAT_1:19, CONLAT_1:def_20; hence ( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) in the carrier of (ConceptLattice C) & S1[e, ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #)] ) by CONLAT_1:31; ::_thesis: verum 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 S1[e,f . e] from FUNCT_2:sch_1(A1); take f ; ::_thesis: for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) let o be Element of C; ::_thesis: ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) thus ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of the carrier of C, the carrier of (ConceptLattice C) st ( for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) & ( for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b2 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) holds b1 = b2 proof let F1, F2 be Function of the carrier of C, the carrier of (ConceptLattice C); ::_thesis: ( ( for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( F1 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) & ( for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( F2 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) implies F1 = F2 ) assume A3: for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( F1 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ; ::_thesis: ( ex o being Element of C st for O being Subset of the carrier of C for A being Subset of the carrier' of C holds ( not F2 . o = ConceptStr(# O,A #) or not O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) or not A = (ObjectDerivation C) . {o} ) or F1 = F2 ) assume A4: for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( F2 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ; ::_thesis: F1 = F2 A5: for o being set st o in the carrier of C holds F1 . o = F2 . o proof let o be set ; ::_thesis: ( o in the carrier of C implies F1 . o = F2 . o ) assume o in the carrier of C ; ::_thesis: F1 . o = F2 . o then reconsider o = o as Element of C ; ( ex O being Subset of the carrier of C ex 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 ex 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 F1 . o = F2 . o ; ::_thesis: verum end; ( dom F1 = the carrier of C & dom F2 = the carrier of C ) by FUNCT_2:def_1; hence F1 = F2 by A5, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def4 defines gamma CONLAT_2:def_4_:_ for C being FormalContext for b2 being Function of the carrier of C, the carrier of (ConceptLattice C) holds ( b2 = gamma C iff for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b2 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ); definition let C be FormalContext; func delta C -> Function of the carrier' of C, the carrier of (ConceptLattice C) means :Def5: :: CONLAT_2:def 5 for a being Element of the carrier' of C ex O being Subset of the carrier of C ex 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 ex b1 being Function of the carrier' of C, the carrier of (ConceptLattice C) st for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) proof defpred S1[ set , set ] means ex O being Subset of the carrier of C ex 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 holds ex u being set st ( u in the carrier of (ConceptLattice C) & S1[e,u] ) proof let e be set ; ::_thesis: ( e in the carrier' of C implies ex u being set st ( u in the carrier of (ConceptLattice C) & S1[e,u] ) ) assume e in the carrier' of C ; ::_thesis: ex u being set st ( u in the carrier of (ConceptLattice C) & S1[e,u] ) 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(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #) ; ::_thesis: ( ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #) in the carrier of (ConceptLattice C) & S1[e, ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #)] ) ( ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) & ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #) is FormalConcept of C ) by CONLAT_1:21, CONLAT_1:def_20; hence ( ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #) in the carrier of (ConceptLattice C) & S1[e, ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #)] ) by CONLAT_1:31; ::_thesis: verum 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 S1[e,f . e] from FUNCT_2:sch_1(A1); take f ; ::_thesis: for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( f . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) let o be Element of the carrier' of C; ::_thesis: ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {o} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {o}) ) thus ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {o} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {o}) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of the carrier' of C, the carrier of (ConceptLattice C) st ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) & ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b2 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) holds b1 = b2 proof let F1, F2 be Function of the carrier' of C, the carrier of (ConceptLattice C); ::_thesis: ( ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( F1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) & ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( F2 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) implies F1 = F2 ) assume A3: for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( F1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ; ::_thesis: ( ex a being Element of the carrier' of C st for O being Subset of the carrier of C for A being Subset of the carrier' of C holds ( not F2 . a = ConceptStr(# O,A #) or not O = (AttributeDerivation C) . {a} or not A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) or F1 = F2 ) assume A4: for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( F2 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ; ::_thesis: F1 = F2 A5: for a being set st a in the carrier' of C holds F1 . a = F2 . a proof let a be set ; ::_thesis: ( a in the carrier' of C implies F1 . a = F2 . a ) assume a in the carrier' of C ; ::_thesis: F1 . a = F2 . a then reconsider a = a as Element of the carrier' of C ; ( ex O being Subset of the carrier of C ex 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 ex 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 F1 . a = F2 . a ; ::_thesis: verum end; ( dom F1 = the carrier' of C & dom F2 = the carrier' of C ) by FUNCT_2:def_1; hence F1 = F2 by A5, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def5 defines delta CONLAT_2:def_5_:_ for C being FormalContext for b2 being Function of the carrier' of C, the carrier of (ConceptLattice C) holds ( b2 = delta C iff for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b2 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ); theorem :: CONLAT_2:11 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; ::_thesis: 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 ) let o be Object of C; ::_thesis: for a being Attribute of C holds ( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C ) let a be Attribute of C; ::_thesis: ( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C ) ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def_20; hence ( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C ) by CONLAT_1:def_15; ::_thesis: verum end; theorem Th12: :: CONLAT_2:12 for C being FormalContext holds ( rng (gamma C) is supremum-dense & rng (delta C) is infimum-dense ) proof let C be FormalContext; ::_thesis: ( rng (gamma C) is supremum-dense & rng (delta C) is infimum-dense ) set G = rng (gamma C); thus rng (gamma C) is supremum-dense ::_thesis: rng (delta C) is infimum-dense proof let a be Element of (ConceptLattice C); :: according to LATTICE6:def_13 ::_thesis: ex b1 being Element of bool (rng (gamma C)) st a = "\/" (b1,(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= rng (gamma C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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} ) } or x in rng (gamma C) ) 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} ) } ; ::_thesis: x in rng (gamma C) 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 ex 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 x in rng (gamma C) by A2, A3, A4, A5, FUNCT_1:def_3; ::_thesis: verum 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 ex b1 being Element of bool (rng (gamma C)) st a = "\/" (b1,(ConceptLattice C)) by A1; ::_thesis: verum end; let b be Element of (ConceptLattice C); :: according to LATTICE6:def_14 ::_thesis: ex b1 being Element of bool (rng (delta C)) st b = "/\" (b1,(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= rng (delta C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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}) ) } or x in rng (delta C) ) 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}) ) } ; ::_thesis: x in rng (delta C) 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 ex 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 x in rng (delta C) by A7, A8, A9, A10, FUNCT_1:def_3; ::_thesis: verum 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 ex b1 being Element of bool (rng (delta C)) st b = "/\" (b1,(ConceptLattice C)) by A6; ::_thesis: verum end; theorem Th13: :: CONLAT_2:13 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; ::_thesis: 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 ) let o be Object of C; ::_thesis: for a being Attribute of C holds ( o is-connected-with a iff (gamma C) . o [= (delta C) . a ) let a be Attribute of C; ::_thesis: ( o is-connected-with a iff (gamma C) . o [= (delta C) . a ) 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 ::_thesis: ( (gamma C) . o [= (delta C) . a implies o is-connected-with a ) assume o is-connected-with a ; ::_thesis: (gamma C) . o [= (delta C) . 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; ::_thesis: verum 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 ; ::_thesis: o is-connected-with 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 {a} c= (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . {o})) by A2, A10, CONLAT_1:11; then {a} c= (ObjectDerivation C) . {o} 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 o is-connected-with a ; ::_thesis: verum end; begin Lm1: for L1, L2 being Lattice for f being Function of the carrier of L1, the carrier of L2 st ( for a, b being Element of L1 st f . a [= f . b holds a [= b ) holds f is one-to-one proof let L1, L2 be Lattice; ::_thesis: for f being Function of the carrier of L1, the carrier of L2 st ( for a, b being Element of L1 st f . a [= f . b holds a [= b ) holds f is one-to-one let f be Function of the carrier of L1, the carrier of L2; ::_thesis: ( ( for a, b being Element of L1 st f . a [= f . b holds a [= b ) implies f is one-to-one ) assume A1: for a, b being Element of L1 st f . a [= f . b holds a [= b ; ::_thesis: f is one-to-one let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y ) assume that A2: x in dom f and A3: y in dom f and A4: f . x = f . y ; ::_thesis: x = y reconsider y = y as Element of L1 by A3; reconsider x = x as Element of L1 by A2; ( x [= y & y [= x ) by A1, A4; hence x = y by LATTICES:8; ::_thesis: verum 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 & ( for a, b being Element of L1 holds ( a [= b iff f . a [= f . b ) ) holds f is Homomorphism of L1,L2 proof let L1, L2 be complete Lattice; ::_thesis: 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 & ( for a, b being Element of L1 holds ( a [= b iff f . a [= f . b ) ) holds f is Homomorphism of L1,L2 let f be Function of the carrier of L1, the carrier of L2; ::_thesis: ( f is one-to-one & rng f = the carrier of L2 & ( for a, b being Element of L1 holds ( a [= b iff f . a [= f . b ) ) implies f is Homomorphism of L1,L2 ) assume A1: ( f is one-to-one & rng f = the carrier of L2 ) ; ::_thesis: ( ex a, b being Element of L1 st ( ( a [= b implies f . a [= f . b ) implies ( f . a [= f . b & not a [= b ) ) or f is Homomorphism of L1,L2 ) assume A2: for a, b being Element of L1 holds ( a [= b iff f . a [= f . b ) ; ::_thesis: f is Homomorphism of L1,L2 A3: for a, b being Element of L1 holds f . (a "/\" b) = (f . a) "/\" (f . b) proof let a, b be Element of L1; ::_thesis: f . (a "/\" b) = (f . a) "/\" (f . b) 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; ::_thesis: ( r is_less_than {(f . a),(f . b)} implies r [= f . (a "/\" b) ) assume A6: r is_less_than {(f . a),(f . b)} ; ::_thesis: r [= f . (a "/\" 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 r [= f . (a "/\" b) by A2, A7; ::_thesis: verum 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 f . (a "/\" b) = (f . a) "/\" (f . b) by LATTICE3:43; ::_thesis: verum end; for a, b being Element of L1 holds f . (a "\/" b) = (f . a) "\/" (f . b) proof let a, b be Element of L1; ::_thesis: f . (a "\/" b) = (f . a) "\/" (f . b) 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; ::_thesis: ( {(f . a),(f . b)} is_less_than r implies f . (a "\/" b) [= r ) assume A12: {(f . a),(f . b)} is_less_than r ; ::_thesis: f . (a "\/" b) [= 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 f . (a "\/" b) [= r by A2, A13; ::_thesis: verum 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 f . (a "\/" b) = (f . a) "\/" (f . b) by LATTICE3:43; ::_thesis: verum end; hence f is Homomorphism of L1,L2 by A3, LATTICE4:def_1; ::_thesis: verum end; Lm3: for C being FormalContext for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds not CS is empty proof let C be FormalContext; ::_thesis: for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds not CS is empty let CS be ConceptStr over C; ::_thesis: ( (ObjectDerivation C) . the Extent of CS = the Intent of CS implies not CS is empty ) assume A1: (ObjectDerivation C) . the Extent of CS = the Intent of CS ; ::_thesis: not CS is empty percases ( the Extent of CS is empty or not the Extent of CS is empty ) ; suppose the Extent of CS is empty ; ::_thesis: not CS is empty then the Intent of CS = the carrier' of C by A1, CONLAT_1:17; hence not CS is empty by CONLAT_1:def_8; ::_thesis: verum end; suppose not the Extent of CS is empty ; ::_thesis: not CS is empty hence not CS is empty by CONLAT_1:def_8; ::_thesis: verum end; end; end; theorem Th14: :: CONLAT_2:14 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 ex 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 for a being Attribute of C holds ( o is-connected-with a iff g . o [= d . a ) ) ) ) proof let L be complete Lattice; ::_thesis: for C being FormalContext holds ( ConceptLattice C,L are_isomorphic iff ex g being Function of the carrier of C, the carrier of L ex 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 for a being Attribute of C holds ( o is-connected-with a iff g . o [= d . a ) ) ) ) let C be FormalContext; ::_thesis: ( ConceptLattice C,L are_isomorphic iff ex g being Function of the carrier of C, the carrier of L ex 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 for a being Attribute of C holds ( o is-connected-with a iff g . o [= d . a ) ) ) ) hereby ::_thesis: ( ex g being Function of the carrier of C, the carrier of L ex 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 for a being Attribute of C holds ( o is-connected-with a iff g . o [= d . a ) ) ) implies ConceptLattice C,L are_isomorphic ) assume ConceptLattice C,L are_isomorphic ; ::_thesis: ex g being Element of bool [: the carrier of C, the carrier of L:] ex d being Element of bool [: 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 for a being Attribute of C holds ( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) ) ) then consider f being Homomorphism of ConceptLattice C,L such that A1: f is bijective by LATTICE4:def_2; take g = f * (gamma C); ::_thesis: ex d being Element of bool [: 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 for a being Attribute of C holds ( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) ) ) take d = f * (delta C); ::_thesis: ( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of C for a being Attribute of C holds ( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) ) ) thus rng g is supremum-dense ::_thesis: ( rng d is infimum-dense & ( for o being Object of C for a being Attribute of C holds ( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) ) ) proof let a be Element of L; :: according to LATTICE6:def_13 ::_thesis: ex b1 being Element of bool (rng g) st a = "\/" (b1,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 { (f . x) where x is Element of (ConceptLattice C) : x in D9 } is_less_than r holds a [= r proof let r be Element of L; ::_thesis: ( { (f . x) where x is Element of (ConceptLattice C) : x in D9 } is_less_than r implies a [= r ) consider r9 being Element of (ConceptLattice C) such that A5: r = f . r9 by A1, LATTICE4:6; reconsider r9 = r9 as Element of (ConceptLattice C) ; assume A6: { (f . x) where x is Element of (ConceptLattice C) : x in D9 } is_less_than r ; ::_thesis: a [= r for q being Element of (ConceptLattice C) st q in D9 holds q [= r9 proof let q be Element of (ConceptLattice C); ::_thesis: ( q in D9 implies q [= r9 ) assume q in D9 ; ::_thesis: q [= r9 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 q [= r9 by A1, LATTICE4:5; ::_thesis: verum end; then D9 is_less_than r9 by LATTICE3:def_17; then b [= r9 by A3, LATTICE3:def_21; hence a [= r by A1, A2, A5, LATTICE4:5; ::_thesis: verum end; A7: { (f . x) where x is Element of (ConceptLattice C) : x in D9 } c= rng g proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } or x in rng g ) assume x in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ; ::_thesis: x in rng g 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 x in rng g by A11, FUNCT_1:def_3; ::_thesis: verum end; A12: D9 is_less_than b by A3, LATTICE3:def_21; { (f . x) where x is Element of (ConceptLattice C) : x in D9 } is_less_than a proof let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } or q [= a ) assume q in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ; ::_thesis: q [= a 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 q [= a by A1, A2, A13, LATTICE4:5; ::_thesis: verum end; then a = "\/" ( { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ,L) by A4, LATTICE3:def_21; hence ex b1 being Element of bool (rng g) st a = "\/" (b1,L) by A7; ::_thesis: verum end; thus rng d is infimum-dense ::_thesis: for o being Object of C for a being Attribute of C holds ( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) proof let a be Element of L; :: according to LATTICE6:def_14 ::_thesis: ex b1 being Element of bool (rng d) st a = "/\" (b1,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 { (f . x) where x is Element of (ConceptLattice C) : x in D9 } holds r [= a proof let r be Element of L; ::_thesis: ( r is_less_than { (f . x) where x is Element of (ConceptLattice C) : x in D9 } implies r [= a ) consider r9 being Element of (ConceptLattice C) such that A18: r = f . r9 by A1, LATTICE4:6; reconsider r9 = r9 as Element of (ConceptLattice C) ; assume A19: r is_less_than { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ; ::_thesis: r [= a r9 is_less_than D9 proof let q be Element of (ConceptLattice C); :: according to LATTICE3:def_16 ::_thesis: ( not q in D9 or r9 [= q ) assume q in D9 ; ::_thesis: r9 [= q 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 r9 [= q by A1, LATTICE4:5; ::_thesis: verum end; then r9 [= b by A16, LATTICE3:34; hence r [= a by A1, A15, A18, LATTICE4:5; ::_thesis: verum end; A20: { (f . x) where x is Element of (ConceptLattice C) : x in D9 } c= rng d proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } or x in rng d ) assume x in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ; ::_thesis: x in rng 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 x in rng d by A24, FUNCT_1:def_3; ::_thesis: verum end; A25: b is_less_than D9 by A16, LATTICE3:34; a is_less_than { (f . x) where x is Element of (ConceptLattice C) : x in D9 } proof let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not q in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } or a [= q ) assume q in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ; ::_thesis: a [= q 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 a [= q by A1, A15, A26, LATTICE4:5; ::_thesis: verum end; then a = "/\" ( { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ,L) by A17, LATTICE3:34; hence ex b1 being Element of bool (rng d) st a = "/\" (b1,L) by A20; ::_thesis: verum end; let o be Object of C; ::_thesis: for a being Attribute of C holds ( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) let a be Attribute of C; ::_thesis: ( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) A28: ( o is-connected-with a iff (gamma C) . o [= (delta C) . a ) by Th13; hereby ::_thesis: ( g . o [= d . a implies o is-connected-with a ) 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 ; ::_thesis: g . o [= d . a hence g . o [= d . a by A1, A28, A30, A29, LATTICE4:5; ::_thesis: verum 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 ; ::_thesis: o is-connected-with a then (gamma C) . o [= (delta C) . a by A1, A31, A32, LATTICE4:5; hence o is-connected-with a by Th13; ::_thesis: verum 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 for a being Attribute of C holds ( o is-connected-with a iff g . o [= d . a ) ; ::_thesis: ConceptLattice C,L are_isomorphic 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: { [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) ) } c= [: the carrier of (ConceptLattice C), the carrier of L:] proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { [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) ) } or y in [: the carrier of (ConceptLattice C), the carrier of L:] ) assume y in { [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) ) } ; ::_thesis: y in [: the carrier of (ConceptLattice C), the carrier of L:] 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 y in [: the carrier of (ConceptLattice C), the carrier of L:] by A38, ZFMISC_1:def_2; ::_thesis: verum end; { [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 } ) } c= [: the carrier of L, the carrier of (ConceptLattice C):] proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { [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 } ) } or y in [: the carrier of L, the carrier of (ConceptLattice C):] ) assume y in { [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 } ) } ; ::_thesis: y in [: the carrier of L, the carrier of (ConceptLattice C):] 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 #) :: according to XBOOLE_0:def_10 ::_thesis: the Extent of ConceptStr(# O,A #) c= (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) or u in the Extent of ConceptStr(# O,A #) ) 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 ; :: according to TARSKI:def_3 ::_thesis: ( not u in D or u in { (d . a9) where a9 is Attribute of C : x [= d . a9 } ) assume A47: u in D ; ::_thesis: u in { (d . a9) where a9 is Attribute of C : x [= d . a9 } then consider v being set such that A48: v in dom d and A49: u = d . v by FUNCT_1:def_3; reconsider v = v as Attribute of C by A48; x [= d . v by A46, A47, A49, LATTICE3:def_16; hence u in { (d . a9) where a9 is Attribute of C : x [= d . a9 } by A49; ::_thesis: verum 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; :: according to LATTICE3:def_16 ::_thesis: ( not u in { (d . a9) where a9 is Attribute of C : x [= d . a9 } or x [= u ) assume u in { (d . a9) where a9 is Attribute of C : x [= d . a9 } ; ::_thesis: x [= u then ex v being Attribute of C st ( u = d . v & x [= d . v ) ; hence x [= u ; ::_thesis: verum end; then x [= "/\" ( { (d . a9) where a9 is Attribute of C : x [= d . a9 } ,L) by LATTICE3:39; hence "/\" ( { (d . a9) where a9 is Attribute of C : x [= d . a9 } ,L) = x by A50, LATTICES:8; ::_thesis: verum end; assume u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) ; ::_thesis: u in the Extent 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; ::_thesis: ( v in { a where a is Attribute of C : x [= d . a } implies g . u9 [= d . v ) assume v in { a where a is Attribute of C : x [= d . a } ; ::_thesis: g . u9 [= d . v then u9 is-connected-with v by A42, A52; hence g . u9 [= d . v by A35; ::_thesis: verum end; g . u9 is_less_than { (d . a) where a is Attribute of C : x [= d . a } proof let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not q in { (d . a) where a is Attribute of C : x [= d . a } or g . u9 [= q ) assume q in { (d . a) where a is Attribute of C : x [= d . a } ; ::_thesis: g . u9 [= q 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 g . u9 [= q by A53, A54; ::_thesis: verum end; then g . u9 [= x by A44, LATTICE3:34; hence u in the Extent of ConceptStr(# O,A #) by A41, A51; ::_thesis: verum end; let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in the Extent of ConceptStr(# O,A #) or u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) ) assume u in the Extent of ConceptStr(# O,A #) ; ::_thesis: u in (AttributeDerivation C) . the Intent 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; ::_thesis: ( v in { a where a is Attribute of C : x [= d . a } implies g . u9 [= d . v ) assume v in { a where a is Attribute of C : x [= d . a } ; ::_thesis: g . u9 [= d . v then ex v9 being Attribute of C st ( v9 = v & x [= d . v9 ) ; hence g . u9 [= d . v by A57, LATTICES:7; ::_thesis: verum 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; ::_thesis: ( v in { a where a is Attribute of C : x [= d . a } implies u9 is-connected-with v ) assume v in { a where a is Attribute of C : x [= d . a } ; ::_thesis: u9 is-connected-with v then g . u9 [= d . v by A58; hence u9 is-connected-with v by A35; ::_thesis: verum 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 u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) by A56, CONLAT_1:def_4; ::_thesis: verum 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 #) :: according to XBOOLE_0:def_10 ::_thesis: the Intent of ConceptStr(# O,A #) c= (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) or u in the Intent of ConceptStr(# O,A #) ) 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 ; :: according to TARSKI:def_3 ::_thesis: ( not u in D or u in { (g . a9) where a9 is Object of C : g . a9 [= x } ) assume A62: u in D ; ::_thesis: u in { (g . a9) where a9 is Object of C : g . a9 [= x } then consider v being set such that A63: v in dom g and A64: u = g . v by FUNCT_1:def_3; reconsider v = v as Object of C by A63; g . v [= x by A61, A62, A64, LATTICE3:def_17; hence u in { (g . a9) where a9 is Object of C : g . a9 [= x } by A64; ::_thesis: verum 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; :: according to LATTICE3:def_17 ::_thesis: ( not u in { (g . a9) where a9 is Object of C : g . a9 [= x } or u [= x ) assume u in { (g . a9) where a9 is Object of C : g . a9 [= x } ; ::_thesis: u [= x then ex v being Object of C st ( u = g . v & g . v [= x ) ; hence u [= x ; ::_thesis: verum end; then "\/" ( { (g . a9) where a9 is Object of C : g . a9 [= x } ,L) [= x by LATTICE3:def_21; hence "\/" ( { (g . a9) where a9 is Object of C : g . a9 [= x } ,L) = x by A65, LATTICES:8; ::_thesis: verum end; assume u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) ; ::_thesis: u in the Intent 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; ::_thesis: ( v in { a where a is Object of C : g . a [= x } implies g . v [= d . u9 ) assume v in { a where a is Object of C : g . a [= x } ; ::_thesis: g . v [= d . u9 then v is-connected-with u9 by A41, A67; hence g . v [= d . u9 by A35; ::_thesis: verum end; { (g . a) where a is Object of C : g . a [= x } is_less_than d . u9 proof let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in { (g . a) where a is Object of C : g . a [= x } or q [= d . u9 ) assume q in { (g . a) where a is Object of C : g . a [= x } ; ::_thesis: q [= d . u9 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 q [= d . u9 by A68, A69; ::_thesis: verum end; then x [= d . u9 by A59, LATTICE3:def_21; hence u in the Intent of ConceptStr(# O,A #) by A42, A66; ::_thesis: verum end; let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in the Intent of ConceptStr(# O,A #) or u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) ) assume u in the Intent of ConceptStr(# O,A #) ; ::_thesis: u in (ObjectDerivation C) . the Extent 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; ::_thesis: ( v in { a where a is Object of C : g . a [= x } implies g . v [= d . u9 ) assume v in { a where a is Object of C : g . a [= x } ; ::_thesis: g . v [= d . u9 then ex v9 being Object of C st ( v9 = v & g . v9 [= x ) ; hence g . v [= d . u9 by A72, LATTICES:7; ::_thesis: verum 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; ::_thesis: ( v in { a where a is Object of C : g . a [= x } implies v is-connected-with u9 ) assume v in { a where a is Object of C : g . a [= x } ; ::_thesis: v is-connected-with u9 then g . v [= d . u9 by A73; hence v is-connected-with u9 by A35; ::_thesis: verum 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 u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) by A71, CONLAT_1:def_3; ::_thesis: verum 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 y in [: the carrier of L, the carrier of (ConceptLattice C):] by A40, ZFMISC_1:def_2; ::_thesis: verum end; then reconsider 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 } ) } 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 ; ::_thesis: ( [x,y1] in fi & [x,y2] in fi implies y1 = y2 ) assume that A75: [x,y1] in fi and A76: [x,y2] in fi ; ::_thesis: y1 = y2 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 ; ::_thesis: verum end; the carrier of L c= dom fi proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of L or y in dom fi ) assume y in the carrier of L ; ::_thesis: y in dom fi then reconsider y = y as Element of L ; set A = { a where a is Attribute of C : y [= d . a } ; { a where a is Attribute of C : y [= d . a } c= the carrier' of C proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a where a is Attribute of C : y [= d . a } or u in the carrier' of C ) assume u in { a where a is Attribute of C : y [= d . a } ; ::_thesis: u in the carrier' of C then ex u9 being Attribute of C st ( u9 = u & y [= d . u9 ) ; hence u in the carrier' of C ; ::_thesis: verum end; then reconsider A = { a where a is Attribute of C : y [= d . a } as Subset of the carrier' of C ; set O = { o where o is Object of C : g . o [= y } ; { o where o is Object of C : g . o [= y } c= the carrier of C proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { o where o is Object of C : g . o [= y } or u in the carrier of C ) assume u in { o where o is Object of C : g . o [= y } ; ::_thesis: u in the carrier of C then ex u9 being Object of C st ( u9 = u & g . u9 [= y ) ; hence u in the carrier of C ; ::_thesis: verum end; then reconsider O = { o where o is Object of C : g . o [= y } as Subset of the carrier of C ; [y,ConceptStr(# O,A #)] in fi ; hence y in dom fi by XTUPLE_0:def_12; ::_thesis: verum end; then A82: the carrier of L = dom fi by XBOOLE_0:def_10; reconsider 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) ) } 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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of (ConceptLattice C) or y in dom f ) assume y in the carrier of (ConceptLattice C) ; ::_thesis: y in dom f 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 y in dom f by XTUPLE_0:def_12; ::_thesis: verum end; then A85: the carrier of (ConceptLattice C) = dom f by XBOOLE_0:def_10; reconsider fi = 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 ; ::_thesis: ( [x,y1] in f & [x,y2] in f implies y1 = y2 ) assume that A86: [x,y1] in f and A87: [x,y2] in f ; ::_thesis: y1 = y2 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 ; ::_thesis: verum end; then reconsider f = 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; ::_thesis: f . (fi . a) = a reconsider a = a as Element of L ; set A = { a9 where a9 is Attribute of C : a [= d . a9 } ; { a9 where a9 is Attribute of C : a [= d . a9 } c= the carrier' of C proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a9 where a9 is Attribute of C : a [= d . a9 } or u in the carrier' of C ) assume u in { a9 where a9 is Attribute of C : a [= d . a9 } ; ::_thesis: u in the carrier' of C then ex u9 being Attribute of C st ( u9 = u & a [= d . u9 ) ; hence u in the carrier' of C ; ::_thesis: verum end; then reconsider A = { a9 where a9 is Attribute of C : a [= d . a9 } as Subset of the carrier' of C ; set O = { o where o is Object of C : g . o [= a } ; { o where o is Object of C : g . o [= a } c= the carrier of C proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { o where o is Object of C : g . o [= a } or u in the carrier of C ) assume u in { o where o is Object of C : g . o [= a } ; ::_thesis: u in the carrier of C then ex u9 being Object of C st ( u9 = u & g . u9 [= a ) ; hence u in the carrier of C ; ::_thesis: verum end; then reconsider O = { o where o is Object of C : g . o [= a } 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 ; :: according to TARSKI:def_3 ::_thesis: ( not u in D or u in { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } ) assume A98: u in D ; ::_thesis: 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 set such that A99: v in dom g and A100: u = g . v by FUNCT_1:def_3; reconsider v = 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 u in { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } by A100; ::_thesis: verum 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; :: according to LATTICE3:def_17 ::_thesis: ( not u in { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } or u [= a ) assume u in { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } ; ::_thesis: u [= 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 u [= a by A102; ::_thesis: verum 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 "\/" ( { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } ,L) = a by A101, LATTICES:8; ::_thesis: verum 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 #),("\/" ( { (g . o) where o is Object of C : o in the Extent of ConceptStr(# O,A #) } ,L))] in f ; then f . ConceptStr(# O,A #) = "\/" ( { (g . o) where o is Object of C : o in the Extent of ConceptStr(# O,A #) } ,L) by FUNCT_1:1; hence f . (fi . a) = a by A104, A95, FUNCT_1:1; ::_thesis: verum end; the carrier of L c= rng f proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in the carrier of L or u in rng f ) A105: dom f = the carrier of (ConceptLattice C) by FUNCT_2:def_1; assume A106: u in the carrier of L ; ::_thesis: u in rng f 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 = u as Element of L by A106; v in rng fi by A107, XTUPLE_0:def_13; then reconsider v = v as Element of (ConceptLattice C) ; f . v = f . (fi . u) by A107, FUNCT_1:1 .= u by A94 ; hence u in rng f by A105, FUNCT_1:def_3; ::_thesis: verum 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); ::_thesis: f . x = "/\" ( { (d . a) where a is Attribute of C : a in the Intent of (x @) } ,L) set y = "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L); A110: [(x @),("\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L))] in f ; A111: for o being set st o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } holds o in { (d . a) where a is Attribute of C : a in the Intent of (x @) } proof let o be set ; ::_thesis: ( o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } implies o in { (d . a) where a is Attribute of C : a in the Intent of (x @) } ) assume o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ; ::_thesis: o in { (d . a) where a is Attribute of C : a in the Intent of (x @) } then consider u being Attribute of C such that A112: o = d . u and A113: "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= 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; ::_thesis: ( o in the Extent of (x @) implies g . o [= d . u ) assume o in the Extent of (x @) ; ::_thesis: g . o [= d . u then g . o in { (g . o9) where o9 is Object of C : o9 in the Extent of (x @) } ; then g . o [= "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by LATTICE3:38; hence g . o [= d . u by A113, LATTICES:7; ::_thesis: verum 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; ::_thesis: ( o in the Extent of (x @) implies o is-connected-with u ) assume o in the Extent of (x @) ; ::_thesis: o is-connected-with u then g . o [= d . u by A114; hence o is-connected-with u by A35; ::_thesis: verum 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 o in { (d . a) where a is Attribute of C : a in the Intent of (x @) } by A112; ::_thesis: verum end; A115: for o9 being Object of C st o9 in the Extent of (x @) holds 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; ::_thesis: ( o9 in the Extent of (x @) implies for a9 being Attribute of C st a9 in the Intent of (x @) holds g . o9 [= d . a9 ) assume A116: o9 in the Extent of (x @) ; ::_thesis: for a9 being Attribute of C st a9 in the Intent of (x @) holds g . o9 [= d . a9 let a9 be Attribute of C; ::_thesis: ( a9 in the Intent of (x @) implies g . o9 [= d . a9 ) assume a9 in the Intent of (x @) ; ::_thesis: g . o9 [= d . a9 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 g . o9 [= d . a9 by A35; ::_thesis: verum end; A117: for o being set st o in { (d . a) where a is Attribute of C : a in the Intent of (x @) } holds o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } proof let o be set ; ::_thesis: ( 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 : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ) assume o in { (d . a) where a is Attribute of C : a in the Intent of (x @) } ; ::_thesis: o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } 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; :: according to LATTICE3:def_17 ::_thesis: ( not q in { (g . o9) where o9 is Object of C : o9 in the Extent of (x @) } or q [= d . b ) assume q in { (g . o9) where o9 is Object of C : o9 in the Extent of (x @) } ; ::_thesis: q [= d . b then ex u being Object of C st ( q = g . u & u in the Extent of (x @) ) ; hence q [= d . b by A115, A119; ::_thesis: verum end; then "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . b by LATTICE3:def_21; hence o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } by A118; ::_thesis: verum end; A120: "/\" ( { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ,L) = "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) proof consider D being Subset of (rng d) such that A121: "/\" (D,L) = "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by A34, LATTICE6:def_14; A122: "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) is_less_than D by A121, LATTICE3:34; D c= { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in D or u in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ) assume A123: u in D ; ::_thesis: u in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } then consider v being set such that A124: v in dom d and A125: u = d . v by FUNCT_1:def_3; reconsider v = v as Attribute of C by A124; "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . v by A122, A123, A125, LATTICE3:def_16; hence u in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } by A125; ::_thesis: verum end; then A126: "/\" ( { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ,L) [= "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by A121, LATTICE3:45; "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) is_less_than { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } proof let u be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not u in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } or "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= u ) assume u in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ; ::_thesis: "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= u then ex v being Attribute of C st ( u = d . v & "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . v ) ; hence "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= u ; ::_thesis: verum end; then "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= "/\" ( { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ,L) by LATTICE3:39; hence "/\" ( { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ,L) = "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by A126, LATTICES:8; ::_thesis: verum end; f . x = f . (x @) by CONLAT_1:def_21 .= "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by A110, FUNCT_1:1 ; hence f . x = "/\" ( { (d . a) where a is Attribute of C : a in the Intent of (x @) } ,L) by A111, A117, A120, TARSKI:1; ::_thesis: verum end; A127: for a being Element of (ConceptLattice C) holds fi . (f . a) = a proof let a be Element of (ConceptLattice C); ::_thesis: fi . (f . a) = a 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 : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } ; { a9 where a9 is Attribute of C : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } c= the carrier' of C proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a9 where a9 is Attribute of C : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } or u in the carrier' of C ) assume u in { a9 where a9 is Attribute of C : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } ; ::_thesis: u in the carrier' of C then ex u9 being Attribute of C st ( u9 = u & "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . u9 ) ; hence u in the carrier' of C ; ::_thesis: verum end; then reconsider A = { a9 where a9 is Attribute of C : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } as Subset of the carrier' of C ; set O = { o where o is Object of C : g . o [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) } ; { o where o is Object of C : g . o [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) } c= the carrier of C proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { o where o is Object of C : g . o [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) } or u in the carrier of C ) assume u in { o where o is Object of C : g . o [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) } ; ::_thesis: u in the carrier of C then ex u9 being Object of C st ( u9 = u & g . u9 [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) ) ; hence u in the carrier of C ; ::_thesis: verum end; then reconsider O = { o where o is Object of C : g . o [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) } 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 } :: according to XBOOLE_0:def_10 ::_thesis: { 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 proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in O or 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 } ) assume u in O ; ::_thesis: 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 A129: u = o9 and A130: g . o9 [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) ; 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; ::_thesis: ( a9 in the Intent of (a @) implies g . o9 [= d . a9 ) assume a9 in the Intent of (a @) ; ::_thesis: g . o9 [= d . a9 then d . a9 in { (d . y) where y is Attribute of C : y in the Intent of (a @) } ; then "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 by LATTICE3:38; hence g . o9 [= d . a9 by A130, LATTICES:7; ::_thesis: verum end; hence 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 } by A129; ::_thesis: verum end; let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or u in O ) 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 } ; ::_thesis: u in O 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; :: according to LATTICE3:def_16 ::_thesis: ( not q in { (d . y) where y is Attribute of C : y in the Intent of (a @) } or g . o9 [= q ) assume q in { (d . y) where y is Attribute of C : y in the Intent of (a @) } ; ::_thesis: g . o9 [= q then ex qa being Attribute of C st ( q = d . qa & qa in the Intent of (a @) ) ; hence g . o9 [= q by A132; ::_thesis: verum end; then g . o9 [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) by LATTICE3:34; hence u in O by A131; ::_thesis: verum 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 } :: according to XBOOLE_0:def_10 ::_thesis: { 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 } 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 ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or 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 } ) 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 } ; ::_thesis: 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 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; ::_thesis: ( a9 in the Intent of (a @) implies u9 is-connected-with a9 ) assume a9 in the Intent of (a @) ; ::_thesis: u9 is-connected-with a9 then g . u9 [= d . a9 by A134; hence u9 is-connected-with a9 by A35; ::_thesis: verum end; hence 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 } by A133; ::_thesis: verum end; let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or 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 } ) 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 } ; ::_thesis: 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 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; ::_thesis: ( a9 in the Intent of (a @) implies g . u9 [= d . a9 ) assume a9 in the Intent of (a @) ; ::_thesis: g . u9 [= d . a9 then u9 is-connected-with a9 by A136; hence g . u9 [= d . a9 by A35; ::_thesis: verum end; hence 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 } by A135; ::_thesis: verum 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; [("/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L)),ConceptStr(# O,A #)] in fi ; then A139: fi . ("/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L)) = 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 fi . (f . a) = a by A138, A139, A137, CONLAT_1:def_21; ::_thesis: verum end; A140: for a, b being Element of L st a [= b holds fi . a [= fi . b proof let a, b be Element of L; ::_thesis: ( a [= b implies fi . a [= fi . b ) set ca = fi . a; set cb = fi . b; assume A141: a [= b ; ::_thesis: fi . a [= fi . 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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in { o where o is Object of C : g . o [= a } or x in { o where o is Object of C : g . o [= b } ) assume x in { o where o is Object of C : g . o [= a } ; ::_thesis: x in { o where o is Object of C : g . o [= b } 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 x in { o where o is Object of C : g . o [= b } by A143; ::_thesis: verum 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 ((fi . b) @) = 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 ((fi . a) @) = Oa by CONLAT_1:def_21; then (fi . a) @ is-SubConcept-of (fi . b) @ by A142, A153, A149, A154, A150, A151, CONLAT_1:def_16; hence fi . a [= fi . b by CONLAT_1:43; ::_thesis: verum end; A155: for a, b being Element of (ConceptLattice C) st f . a [= f . b holds a [= b proof let a, b be Element of (ConceptLattice C); ::_thesis: ( f . a [= f . b implies a [= b ) assume A156: f . a [= f . b ; ::_thesis: a [= b ( fi . (f . a) = a & fi . (f . b) = b ) by A127; hence a [= b by A140, A156; ::_thesis: verum end; for a, b being Element of (ConceptLattice C) st a [= b holds f . a [= f . b proof let a, b be Element of (ConceptLattice C); ::_thesis: ( a [= b implies f . a [= f . b ) 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 ; ::_thesis: f . a [= f . 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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (g . o) where o is Object of C : o in the Extent of (a @) } or x in { (g . o) where o is Object of C : o in the Extent of (b @) } ) assume x in { (g . o) where o is Object of C : o in the Extent of (a @) } ; ::_thesis: x in { (g . o) where o is Object of C : o in the Extent of (b @) } then ex o being Object of C st ( x = g . o & o in the Extent of (a @) ) ; hence x in { (g . o) where o is Object of C : o in the Extent of (b @) } by A159; ::_thesis: verum end; ( a @ = a & b @ = b ) by CONLAT_1:def_21; hence f . a [= f . b by A160, A157, A158, LATTICE3:45; ::_thesis: verum end; then reconsider f = 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 ConceptLattice C,L are_isomorphic by A161, LATTICE4:def_2; ::_thesis: verum end; definition let L be Lattice; func Context L -> non quasi-empty strict ContextStr equals :: CONLAT_2:def 6 ContextStr(# the carrier of L, the carrier of L,(LattRel L) #); coherence ContextStr(# the carrier of L, the carrier of L,(LattRel L) #) is non quasi-empty strict ContextStr by CONLAT_1:def_1; end; :: deftheorem defines Context CONLAT_2:def_6_:_ for L being Lattice holds Context L = ContextStr(# the carrier of L, the carrier of L,(LattRel L) #); theorem Th15: :: CONLAT_2:15 for L being complete Lattice holds ConceptLattice (Context L),L are_isomorphic proof let L be complete Lattice; ::_thesis: ConceptLattice (Context L),L are_isomorphic 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) for 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); ::_thesis: for a being Attribute of (Context L) holds ( o is-connected-with a iff g . o [= d . a ) let a be Attribute of (Context L); ::_thesis: ( o is-connected-with a iff g . o [= d . a ) 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 ( o is-connected-with a iff g . o [= d . a ) by A2, FILTER_1:31; ::_thesis: verum end; for a being Element of L ex D9 being Subset of (rng d) st a = "/\" (D9,L) proof let a be Element of L; ::_thesis: ex D9 being Subset of (rng d) st a = "/\" (D9,L) ( "/\" ({a},L) = a & rng d = the carrier of L ) by LATTICE3:42, RELAT_1:45; hence ex D9 being Subset of (rng d) st a = "/\" (D9,L) ; ::_thesis: verum end; then A3: rng d is infimum-dense by LATTICE6:def_14; rng g is supremum-dense proof let a be Element of L; :: according to LATTICE6:def_13 ::_thesis: ex b1 being Element of bool (rng g) st a = "\/" (b1,L) ( "\/" ({a},L) = a & rng g = the carrier of L ) by LATTICE3:42, RELAT_1:45; hence ex b1 being Element of bool (rng g) st a = "\/" (b1,L) ; ::_thesis: verum end; hence ConceptLattice (Context L),L are_isomorphic by A3, A1, Th14; ::_thesis: verum end; theorem :: CONLAT_2:16 for L being Lattice holds ( L is complete iff ex C being FormalContext st ConceptLattice C,L are_isomorphic ) proof let L be Lattice; ::_thesis: ( L is complete iff ex C being FormalContext st ConceptLattice C,L are_isomorphic ) hereby ::_thesis: ( ex C being FormalContext st ConceptLattice C,L are_isomorphic implies L is complete ) assume L is complete ; ::_thesis: ex C being FormalContext st ConceptLattice C,L are_isomorphic then ConceptLattice (Context L),L are_isomorphic by Th15; hence ex C being FormalContext st ConceptLattice C,L are_isomorphic ; ::_thesis: verum end; given C being FormalContext such that A1: ConceptLattice C,L are_isomorphic ; ::_thesis: L is complete let X be Subset of L; :: according to VECTSP_8:def_6 ::_thesis: ex b1 being Element of the carrier of L st ( b1 is_less_than X & ( for b2 being Element of the carrier of L holds ( not b2 is_less_than X or b2 [= b1 ) ) ) 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 } ; { (f . x) where x is Element of L : x in X } c= the carrier of (ConceptLattice C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f . x) where x is Element of L : x in X } or x in the carrier of (ConceptLattice C) ) assume x in { (f . x) where x is Element of L : x in X } ; ::_thesis: x in the carrier of (ConceptLattice C) then ex y being Element of L st ( x = f . y & y in X ) ; hence x in the carrier of (ConceptLattice C) ; ::_thesis: verum end; then reconsider FX = { (f . x) where x is Element of L : x in X } as Subset of (ConceptLattice C) ; set Fa = "/\" (FX,(ConceptLattice C)); consider a being Element of L such that A3: "/\" (FX,(ConceptLattice C)) = 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; ::_thesis: ( b is_less_than X implies b [= a ) assume A5: b is_less_than X ; ::_thesis: b [= a f . b is_less_than FX proof let q be Element of (ConceptLattice C); :: according to LATTICE3:def_16 ::_thesis: ( not q in FX or f . b [= q ) assume q in FX ; ::_thesis: f . b [= q 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 f . b [= q by A2, A6, LATTICE4:5; ::_thesis: verum end; then f . b [= f . a by A3, LATTICE3:34; hence b [= a by A2, LATTICE4:5; ::_thesis: verum end; A8: "/\" (FX,(ConceptLattice C)) is_less_than FX by LATTICE3:34; a is_less_than X proof let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not q in X or a [= q ) assume q in X ; ::_thesis: a [= q then f . q in FX ; then "/\" (FX,(ConceptLattice C)) [= f . q by A8, LATTICE3:def_16; hence a [= q by A2, A3, LATTICE4:5; ::_thesis: verum end; hence ex b1 being Element of the carrier of L st ( b1 is_less_than X & ( for b2 being Element of the carrier of L holds ( not b2 is_less_than X or b2 [= b1 ) ) ) by A4; ::_thesis: verum end; begin registration let L be complete Lattice; clusterL .: -> complete ; coherence L .: is complete proof let X be Subset of (L .:); :: according to VECTSP_8:def_6 ::_thesis: ex b1 being Element of the carrier of (L .:) st ( b1 is_less_than X & ( for b2 being Element of the carrier of (L .:) holds ( not b2 is_less_than X or b2 [= b1 ) ) ) 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 = "\/" (X9,L) 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 .:); ::_thesis: ( b is_less_than X implies b [= a ) reconsider b9 = b as Element of L by A1; assume A4: b is_less_than X ; ::_thesis: b [= a X9 is_less_than b9 proof let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in X9 or q [= b9 ) reconsider q9 = q as Element of (L .:) by A1; assume q in X9 ; ::_thesis: q [= b9 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 q [= b9 by LATTICE3:7; ::_thesis: verum end; then "\/" (X9,L) [= b9 by LATTICE3:def_21; then ("\/" (X9,L)) % <= b9 % by LATTICE3:7; then [(("\/" (X9,L)) %),(b9 %)] in the InternalRel of (LattPOSet L) by ORDERS_2:def_5; then [(b9 %),(("\/" (X9,L)) %)] in the InternalRel of (LattPOSet L) ~ by RELAT_1:def_7; then [(b9 %),(("\/" (X9,L)) %)] in the InternalRel of (LattPOSet (L .:)) by LATTICE3:20; then b % <= a % by ORDERS_2:def_5; hence b [= a by LATTICE3:7; ::_thesis: verum end; A5: X9 is_less_than "\/" (X9,L) by LATTICE3:def_21; a is_less_than X proof let q9 be Element of (L .:); :: according to LATTICE3:def_16 ::_thesis: ( not q9 in X or a [= q9 ) reconsider q = q9 as Element of L by A1; assume q9 in X ; ::_thesis: a [= q9 then q [= "\/" (X9,L) by A5, LATTICE3:def_17; then q % <= ("\/" (X9,L)) % by LATTICE3:7; then [(q %),(("\/" (X9,L)) %)] in the InternalRel of (LattPOSet L) by ORDERS_2:def_5; then [(("\/" (X9,L)) %),(q %)] in the InternalRel of (LattPOSet L) ~ by RELAT_1:def_7; then [(("\/" (X9,L)) %),(q %)] in the InternalRel of (LattPOSet (L .:)) by LATTICE3:20; then a % <= q9 % by ORDERS_2:def_5; hence a [= q9 by LATTICE3:7; ::_thesis: verum end; hence ex b1 being Element of the carrier of (L .:) st ( b1 is_less_than X & ( for b2 being Element of the carrier of (L .:) holds ( not b2 is_less_than X or b2 [= b1 ) ) ) by A3; ::_thesis: verum end; end; definition let C be FormalContext; funcC .: -> non quasi-empty strict ContextStr equals :: CONLAT_2:def 7 ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #); coherence ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is non quasi-empty strict ContextStr by CONLAT_1:def_1; end; :: deftheorem defines .: CONLAT_2:def_7_:_ for C being FormalContext holds C .: = ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #); theorem :: CONLAT_2:17 for C being strict FormalContext holds (C .:) .: = C ; theorem Th18: :: CONLAT_2:18 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; ::_thesis: for O being Subset of the carrier of C holds (ObjectDerivation C) . O = (AttributeDerivation (C .:)) . O let O be Subset of the carrier of C; ::_thesis: (ObjectDerivation C) . O = (AttributeDerivation (C .:)) . O 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: { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } c= { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds a is-connected-with o } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } or u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds a is-connected-with o } ) assume u in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } ; ::_thesis: u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds a is-connected-with o } 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 .:); ::_thesis: ( o9 in O9 implies u9 is-connected-with o9 ) reconsider o = o9 as Object of C ; assume o9 in O9 ; ::_thesis: u9 is-connected-with 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 u9 is-connected-with o9 by A2, CONLAT_1:def_2; ::_thesis: verum end; hence u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds a is-connected-with o } ; ::_thesis: verum end; A4: { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds a is-connected-with o } c= { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds a is-connected-with o } or u in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } ) assume u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds a is-connected-with o } ; ::_thesis: u in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } 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; ::_thesis: ( o9 in O implies o9 is-connected-with u9 ) reconsider o = o9 as Attribute of (C .:) ; assume o9 in O ; ::_thesis: o9 is-connected-with u9 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 o9 is-connected-with u9 by CONLAT_1:def_2; ::_thesis: verum end; hence u in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } ; ::_thesis: verum 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, CONLAT_1:def_4; hence (ObjectDerivation C) . O = (AttributeDerivation (C .:)) . O by A1, A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th19: :: CONLAT_2:19 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; ::_thesis: for A being Subset of the carrier' of C holds (AttributeDerivation C) . A = (ObjectDerivation (C .:)) . A let O be Subset of the carrier' of C; ::_thesis: (AttributeDerivation C) . O = (ObjectDerivation (C .:)) . O 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: { a where a is Object of C : for o being Attribute of C st o in O holds a is-connected-with o } c= { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds o is-connected-with a } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a where a is Object of C : for o being Attribute of C st o in O holds a is-connected-with o } or u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds o is-connected-with a } ) assume u in { a where a is Object of C : for o being Attribute of C st o in O holds a is-connected-with o } ; ::_thesis: u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds o is-connected-with a } 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 .:); ::_thesis: ( o9 in O9 implies o9 is-connected-with u9 ) reconsider o = o9 as Attribute of C ; assume o9 in O9 ; ::_thesis: o9 is-connected-with u9 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 o9 is-connected-with u9 by CONLAT_1:def_2; ::_thesis: verum end; hence u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds o is-connected-with a } ; ::_thesis: verum end; A4: { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds o is-connected-with a } c= { a where a is Object of C : for o being Attribute of C st o in O holds a is-connected-with o } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds o is-connected-with a } or u in { a where a is Object of C : for o being Attribute of C st o in O holds a is-connected-with o } ) assume u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds o is-connected-with a } ; ::_thesis: u in { a where a is Object of C : for o being Attribute of C st o in O holds a is-connected-with o } 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; ::_thesis: ( o9 in O implies u9 is-connected-with o9 ) reconsider o = o9 as Object of (C .:) ; assume o9 in O ; ::_thesis: u9 is-connected-with o9 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 u9 is-connected-with o9 by CONLAT_1:def_2; ::_thesis: verum end; hence u in { a where a is Object of C : for o being Attribute of C st o in O holds a is-connected-with o } ; ::_thesis: verum 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, CONLAT_1:def_4; hence (AttributeDerivation C) . O = (ObjectDerivation (C .:)) . O by A1, A4, XBOOLE_0:def_10; ::_thesis: verum end; definition let C be FormalContext; let CP be ConceptStr over C; funcCP .: -> strict ConceptStr over C .: means :Def8: :: CONLAT_2:def 8 ( the Extent of it = the Intent of CP & the Intent of it = the Extent of CP ); existence ex b1 being strict ConceptStr over C .: st ( the Extent of b1 = the Intent of CP & the Intent of b1 = the Extent of CP ) 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 #) ; ::_thesis: ( the Extent of ConceptStr(# O,A #) = the Intent of CP & the Intent of ConceptStr(# O,A #) = the Extent of CP ) thus ( the Extent of ConceptStr(# O,A #) = the Intent of CP & the Intent of ConceptStr(# O,A #) = the Extent of CP ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict ConceptStr over C .: st the Extent of b1 = the Intent of CP & the Intent of b1 = the Extent of CP & the Extent of b2 = the Intent of CP & the Intent of b2 = the Extent of CP holds b1 = b2 ; end; :: deftheorem Def8 defines .: CONLAT_2:def_8_:_ for C being FormalContext for CP being ConceptStr over C for b3 being strict ConceptStr over C .: holds ( b3 = CP .: iff ( the Extent of b3 = the Intent of CP & the Intent of b3 = the Extent of CP ) ); registration let C be FormalContext; let CP be FormalConcept of C; clusterCP .: -> strict non empty concept-like ; coherence ( not CP .: is empty & CP .: is concept-like ) 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 ConceptStr(# O,A #) = (ObjectDerivation C) . the Extent of CP by Th18 .= the Extent of ConceptStr(# O,A #) by CONLAT_1:def_10 ; A2: ConceptStr(# O,A #) = CP .: by Def8; (ObjectDerivation (C .:)) . the Extent of ConceptStr(# O,A #) = (AttributeDerivation C) . the Intent of CP by Th19 .= the Intent of ConceptStr(# O,A #) by CONLAT_1:def_10 ; hence ( not CP .: is empty & CP .: is concept-like ) by A1, A2, Lm3, CONLAT_1:def_10; ::_thesis: verum end; end; theorem :: CONLAT_2:20 for C being strict FormalContext for CP being strict FormalConcept of C holds (CP .:) .: = CP proof let C be strict FormalContext; ::_thesis: for CP being strict FormalConcept of C holds (CP .:) .: = CP let CP be strict FormalConcept of C; ::_thesis: (CP .:) .: = CP 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 (CP .:) .: = CP by A1; ::_thesis: verum end; definition let C be FormalContext; func DualHomomorphism C -> Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) means :Def9: :: CONLAT_2:def 9 for CP being strict FormalConcept of C holds it . CP = CP .: ; existence ex b1 being Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) st for CP being strict FormalConcept of C holds b1 . CP = CP .: 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; { [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 } c= [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):] proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { [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 } or y in [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):] ) assume y in { [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 } ; ::_thesis: y in [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):] 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 y in [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):] by A4, A6, ZFMISC_1:def_2; ::_thesis: verum end; then reconsider 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 } 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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of ((ConceptLattice C) .:) or y in dom f ) assume y in the carrier of ((ConceptLattice C) .:) ; ::_thesis: y in dom f 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 = ConceptStr(# O9,A9 #) .: as Element of (ConceptLattice (C .:)) by A1, CONLAT_1:31; [y,z] in f by A7, A8; hence y in dom f by XTUPLE_0:def_12; ::_thesis: verum 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 ; ::_thesis: ( [x,y1] in f & [x,y2] in f implies y1 = y2 ) assume that A10: [x,y1] in f and A11: [x,y2] in f ; ::_thesis: y1 = y2 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 ; ::_thesis: verum end; then reconsider f = 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) .:) st a [= b holds f . a [= f . b proof let a, b be Element of ((ConceptLattice C) .:); ::_thesis: ( a [= b implies f . a [= f . b ) 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 ; ::_thesis: f . a [= f . 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 = 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 = 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 f . a [= f . b by A27, A23, CONLAT_1:43; ::_thesis: verum end; the carrier of (ConceptLattice (C .:)) c= rng f proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in the carrier of (ConceptLattice (C .:)) or u in rng f ) A31: dom f = the carrier of ((ConceptLattice C) .:) by FUNCT_2:def_1; assume u in the carrier of (ConceptLattice (C .:)) ; ::_thesis: u in rng f then reconsider u = 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 or not the Intent of (u @) is empty ) by CONLAT_1:def_8; A33: (AttributeDerivation C) . the Intent of ConceptStr(# A9,O9 #) = (ObjectDerivation (C .:)) . the Extent of (u @) by Th19 .= the Extent of ConceptStr(# A9,O9 #) by CONLAT_1:def_10 ; (ObjectDerivation C) . the Extent of ConceptStr(# A9,O9 #) = (AttributeDerivation (C .:)) . the Intent of (u @) by Th18 .= the Intent of ConceptStr(# A9,O9 #) by CONLAT_1:def_10 ; then ConceptStr(# A9,O9 #) is FormalConcept of C by A33, A32, CONLAT_1:def_8, CONLAT_1:def_10; then ConceptStr(# A9,O9 #) in dom f by A15, A2, A31, CONLAT_1:31; then consider v being set such that A34: [ConceptStr(# A9,O9 #),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: [ConceptStr(# A9,O9 #),v] = [ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .:)] and ConceptStr(# Ov,Av #) is FormalConcept of C by A34; A36: ConceptStr(# A9,O9 #) = [ConceptStr(# A9,O9 #),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 = v as strict FormalConcept of C .: by A1, CONLAT_1:31; v = [ConceptStr(# A9,O9 #),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 u in rng f by A37, CONLAT_1:def_21; ::_thesis: verum 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 ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b ) assume that A40: a in dom f and A41: b in dom f and A42: f . a = f . b ; ::_thesis: a = b reconsider a = a, b = 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 a = b by A47, A49, A51; ::_thesis: verum end; for a, b being Element of ((ConceptLattice C) .:) st f . a [= f . b holds a [= b proof let a, b be Element of ((ConceptLattice C) .:); ::_thesis: ( f . a [= f . b implies a [= b ) 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 ; ::_thesis: a [= 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 = 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 = 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 a [= b by LATTICE3:7; ::_thesis: verum end; then reconsider f = 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; ::_thesis: f . CP = CP .: 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 = 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 f . CP = CP .: by A65, A68, FUNCT_1:1; ::_thesis: verum end; hence ex b1 being Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) st for CP being strict FormalConcept of C holds b1 . CP = CP .: ; ::_thesis: verum end; uniqueness for b1, b2 being Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) st ( for CP being strict FormalConcept of C holds b1 . CP = CP .: ) & ( for CP being strict FormalConcept of C holds b2 . CP = CP .: ) holds b1 = b2 proof let F1, F2 be Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:); ::_thesis: ( ( for CP being strict FormalConcept of C holds F1 . CP = CP .: ) & ( for CP being strict FormalConcept of C holds F2 . CP = CP .: ) implies F1 = F2 ) assume A69: for CP being strict FormalConcept of C holds F1 . CP = CP .: ; ::_thesis: ( ex CP being strict FormalConcept of C st not F2 . CP = CP .: or F1 = F2 ) assume A70: for CP being strict FormalConcept of C holds F2 . CP = CP .: ; ::_thesis: F1 = F2 A71: for u being set st u in the carrier of ((ConceptLattice C) .:) holds F1 . u = F2 . u proof let u be set ; ::_thesis: ( u in the carrier of ((ConceptLattice C) .:) implies F1 . u = F2 . u ) 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) .:) ; ::_thesis: F1 . u = F2 . u then reconsider u = u as strict FormalConcept of C by A72, CONLAT_1:31; F1 . u = u .: by A69 .= F2 . u by A70 ; hence F1 . u = F2 . u ; ::_thesis: verum end; ( dom F1 = the carrier of ((ConceptLattice C) .:) & dom F2 = the carrier of ((ConceptLattice C) .:) ) by FUNCT_2:def_1; hence F1 = F2 by A71, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def9 defines DualHomomorphism CONLAT_2:def_9_:_ for C being FormalContext for b2 being Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) holds ( b2 = DualHomomorphism C iff for CP being strict FormalConcept of C holds b2 . CP = CP .: ); theorem Th21: :: CONLAT_2:21 for C being FormalContext holds DualHomomorphism C is bijective proof let C be FormalContext; ::_thesis: DualHomomorphism C is bijective 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 (DualHomomorphism C) proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in the carrier of (ConceptLattice (C .:)) or u in rng (DualHomomorphism C) ) assume u in the carrier of (ConceptLattice (C .:)) ; ::_thesis: u in rng (DualHomomorphism C) then reconsider u = 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 or not the Intent of (u @) is empty ) by CONLAT_1:def_8; A4: (AttributeDerivation C) . the Intent of ConceptStr(# A9,O9 #) = (ObjectDerivation (C .:)) . the Extent of (u @) by Th19 .= the Extent of ConceptStr(# A9,O9 #) by CONLAT_1:def_10 ; A5: (ObjectDerivation C) . the Extent of ConceptStr(# A9,O9 #) = (AttributeDerivation (C .:)) . the Intent of (u @) by Th18 .= the Intent of ConceptStr(# A9,O9 #) by CONLAT_1:def_10 ; then ConceptStr(# A9,O9 #) is FormalConcept of C by A4, A3, CONLAT_1:def_8, CONLAT_1:def_10; then A6: ConceptStr(# A9,O9 #) in the carrier of (ConceptLattice C) by A1, CONLAT_1:31; reconsider CP = ConceptStr(# A9,O9 #) as strict FormalConcept of C by A5, A4, A3, CONLAT_1:def_8, CONLAT_1:def_10; A7: the Extent of (CP .:) = the Extent of (u @) by Def8; ( (DualHomomorphism C) . CP = CP .: & the Intent of (CP .:) = the Intent of (u @) ) by Def8, Def9; then A8: (DualHomomorphism C) . CP = u by A7, CONLAT_1:def_21; CP in dom (DualHomomorphism C) by A2, A6, FUNCT_2:def_1; hence u in rng (DualHomomorphism C) by A8, FUNCT_1:def_3; ::_thesis: verum end; then rng (DualHomomorphism C) = the carrier of (ConceptLattice (C .:)) by XBOOLE_0:def_10; then A9: DualHomomorphism C is onto by FUNCT_2:def_3; DualHomomorphism C is one-to-one proof let a, b be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in proj1 (DualHomomorphism C) or not b in proj1 (DualHomomorphism C) or not (DualHomomorphism C) . a = (DualHomomorphism C) . b or a = b ) assume that A10: ( a in dom (DualHomomorphism C) & b in dom (DualHomomorphism C) ) and A11: (DualHomomorphism C) . a = (DualHomomorphism C) . b ; ::_thesis: a = b reconsider a = a, b = 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 = a, b = b as Element of (ConceptLattice C) ; A12: ( (DualHomomorphism C) . (a @) = (DualHomomorphism C) . a & (DualHomomorphism C) . (b @) = (DualHomomorphism C) . b ) by CONLAT_1:def_21; A13: ( (DualHomomorphism C) . (a @) = (a @) .: & (DualHomomorphism C) . (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 a = b ; ::_thesis: verum end; hence DualHomomorphism C is bijective by A9; ::_thesis: verum end; theorem :: CONLAT_2:22 for C being FormalContext holds ConceptLattice (C .:),(ConceptLattice C) .: are_isomorphic proof let C be FormalContext; ::_thesis: ConceptLattice (C .:),(ConceptLattice C) .: are_isomorphic DualHomomorphism C is bijective by Th21; hence ConceptLattice (C .:),(ConceptLattice C) .: are_isomorphic by LATTICE4:def_2; ::_thesis: verum end;