:: Introduction to Concept Lattices :: by Christoph Schwarzweller :: :: Received October 2, 1998 :: Copyright (c) 1998-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies STRUCT_0, XBOOLE_0, RELAT_1, CAT_1, SUBSET_1, TARSKI, FUNCT_1, ZFMISC_1, MCART_1, YELLOW_1, LATTICE3, ORDERS_2, FILTER_1, WAYBEL_1, WAYBEL_0, XXREAL_0, PBOOLE, EQREL_1, CLASSES2, BINOP_1, LATTICES, QC_LANG1, REWRITE1, SETFAM_1, CONLAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, LATTICES, ORDERS_2, YELLOW_1, WAYBEL_1, LATTICE3, SETFAM_1, WAYBEL_0; constructors BINOP_1, DOMAIN_1, LATTICE3, WAYBEL_1, RELSET_1, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICES, LATTICE3, YELLOW_1, XTUPLE_0; requirements SUBSET, BOOLE; definitions TARSKI; equalities TARSKI, BINOP_1; expansions TARSKI; theorems TARSKI, RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, LATTICES, LATTICE3, YELLOW_1, ORDERS_2, FILTER_1, VECTSP_8, SETFAM_1, WAYBEL_0, RELSET_1, XBOOLE_0, XBOOLE_1, XTUPLE_0; schemes BINOP_1; begin registration cluster strict non empty non void for 2-sorted; existence proof 2-sorted(#{{}},{{}}#) is non empty non void; hence thesis; end; end; definition ::$CD struct (2-sorted) ContextStr (# carrier, carrier' -> set, Information -> Relation of the carrier,the carrier' #); end; registration cluster strict non empty non void for ContextStr; existence proof ContextStr(#{{}},{{}},the Relation of {{}},{{}}#) is non empty non void; hence thesis; end; end; definition mode FormalContext is non empty non void ContextStr; end; definition let C be 2-sorted; mode Object of C is Element of C; mode Attribute of C is Element of the carrier' of C; end; registration let C be non empty non void 2-sorted; cluster the carrier' of C -> non empty; coherence; cluster the carrier of C -> non empty; coherence; end; registration let C be non empty non void 2-sorted; cluster non empty for Subset of the carrier of C; existence proof take the carrier of C; the carrier of C c= the carrier of C; hence thesis; end; cluster non empty for Subset of the carrier' of C; existence proof take the carrier' of C; the carrier' of C c= the carrier' of C; hence thesis; end; end; definition let C be FormalContext; let o be Object of C; let a be Attribute of C; pred o is-connected-with a means [o,a] in the Information of C; end; notation let C be FormalContext; let o be Object of C; let a be Attribute of C; antonym o is-not-connected-with a for o is-connected-with a; end; :: Derivation Operators begin definition let C be FormalContext; func ObjectDerivation(C) -> Function of bool the carrier of C,bool the carrier' of C means :Def2: for O being Subset of the carrier of C holds it.O = { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a }; existence proof set f = the set of all [O,{a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}] where O is Subset of the carrier of C ; for u being object st u in f holds ex v,w being object st u = [v,w] proof let u be object; assume u in f; then ex O being Subset of the carrier of C st u = [O,{a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a} ]; hence thesis; end; then reconsider f as Relation by RELAT_1:def 1; for u,v1,v2 being object st [u,v1] in f & [u,v2] in f holds v1 = v2 proof let u,v1,v2 be object; assume that A1: [u,v1] in f and A2: [u,v2] in f; consider O being Subset of the carrier of C such that A3: [u,v1] = [O,{a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}] by A1; A4: v1 = [u,v1]`2 .= [O,{a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}]`2 by A3 .= {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}; consider O9 being Subset of the carrier of C such that A5: [u,v2] = [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 A2; A6: v2 = [u,v2]`2 .= [O9,{a where a is Attribute of C : for o being Object of C st o in O9 holds o is-connected-with a}]`2 by A5 .= {a where a is Attribute of C : for o being Object of C st o in O9 holds o is-connected-with a} ; O = [O,{a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}]`1 .= [u,v1]`1 by A3 .= u .= [u,v2]`1 .= [O9,{a where a is Attribute of C : for o being Object of C st o in O9 holds o is-connected-with a}]`1 by A5 .= O9; hence thesis by A4,A6; end; then reconsider f as Function by FUNCT_1:def 1; A7: for x being object holds x in dom f implies x in bool the carrier of C proof let x be object; assume x in dom f; then consider y being object such that A8: [x,y] in f by XTUPLE_0:def 12; consider O being Subset of the carrier of C such that A9: [x,y] = [O,{a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}] by A8; x = [x,y]`1 .= [O,{a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}]`1 by A9 .= O; hence thesis; end; for x being object holds x in bool the carrier of C implies x in dom f proof let x be object; assume x in bool the carrier of C; then reconsider x as Subset of the carrier of C; [x,{a where a is Attribute of C : for o being Object of C st o in x holds o is-connected-with a}] in f; hence thesis by XTUPLE_0:def 12; end; then A10: dom f = bool the carrier of C by A7,TARSKI:2; rng f c= bool the carrier' of C proof let y be object; assume y in rng f; then consider x being object such that A11: [x,y] in f by XTUPLE_0:def 13; consider O being Subset of the carrier of C such that A12: [x,y] = [O,{a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}] by A11; A13: {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a} c= the carrier' of C proof let u be object; 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}; then ex u9 being Attribute of C st u9 = u & for o being Object of C st o in O holds o is-connected-with u9; hence thesis; end; y = [x,y]`2 .= [O,{a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}]`2 by A12 .= {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}; hence thesis by A13; end; then reconsider f as Function of bool the carrier of C,bool the carrier' of C by A10,FUNCT_2:def 1,RELSET_1:4; take f; for O being Subset of the carrier of C holds f.O = {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 O be Subset of the carrier of C; consider y being object such that A14: [O,y] in f by A10,XTUPLE_0:def 12; consider O9 being Subset of the carrier of C such that A15: [O,y] = [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 A14; A16: y = [O,y]`2 .= [O9,{a where a is Attribute of C : for o being Object of C st o in O9 holds o is-connected-with a}]`2 by A15 .= {a where a is Attribute of C : for o being Object of C st o in O9 holds o is-connected-with a}; O = [O,y]`1 .= [O9,{a where a is Attribute of C : for o being Object of C st o in O9 holds o is-connected-with a}]`1 by A15 .= O9; hence thesis by A10,A14,A16,FUNCT_1:def 2; end; hence thesis; end; uniqueness proof let F1,F2 be Function of bool the carrier of C,bool the carrier' of C; assume A17: for O being Subset of the carrier of C holds F1.O = {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a} ; assume A18: for O being Subset of the carrier of C holds F2.O = {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a} ; A19: for O being object st O in bool the carrier of C holds F1.O = F2.O proof let O be object; assume O in bool the carrier of C; then reconsider O as Subset of the carrier of C; F1.O = {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a} by A17 .= F2.O by A18; hence thesis; end; dom F1 = bool the carrier of C & dom F2 = bool the carrier of C by FUNCT_2:def 1; hence thesis by A19,FUNCT_1:2; end; end; definition let C be FormalContext; func AttributeDerivation(C) -> Function of bool the carrier' of C,bool the carrier of C means :Def3: for A being Subset of the carrier' of C holds it.A = { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a }; existence proof set f = the set of all [A,{o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}] where A is Subset of the carrier' of C ; for u being object st u in f holds ex v,w being object st u = [v,w] proof let u be object; assume u in f; then ex A being Subset of the carrier' of C st u = [A,{o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}] ; hence thesis; end; then reconsider f as Relation by RELAT_1:def 1; for u,v1,v2 being object st [u,v1] in f & [u,v2] in f holds v1 = v2 proof let u,v1,v2 be object; assume that A1: [u,v1] in f and A2: [u,v2] in f; consider A being Subset of the carrier' of C such that A3: [u,v1] = [A,{o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}] by A1; A4: v1 =[u,v1]`2 .= [A,{o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}]`2 by A3 .= {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}; consider A9 being Subset of the carrier' of C such that A5: [u,v2] = [A9,{o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a}] by A2; A6: v2 = [u,v2]`2 .=[A9,{o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a}]`2 by A5 .= [A9,{o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a}] `2 .= {o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a}; A = [A,{o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}]`1 .= [u,v1]`1 by A3 .= u .= [u,v2]`1 .= [A9,{o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a}]`1 by A5 .= A9; hence thesis by A4,A6; end; then reconsider f as Function by FUNCT_1:def 1; A7: for x being object holds x in dom f implies x in bool the carrier' of C proof let x be object; assume x in dom f; then consider y being object such that A8: [x,y] in f by XTUPLE_0:def 12; consider A being Subset of the carrier' of C such that A9: [x,y] = [A,{o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}] by A8; x = [x,y]`1 .=[A,{o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}]`1 by A9 .= A; hence thesis; end; for x being object holds x in bool the carrier' of C implies x in dom f proof let x be object; assume x in bool the carrier' of C; then reconsider x as Subset of the carrier' of C; [x,{o where o is Object of C : for a being Attribute of C st a in x holds o is-connected-with a}] in f; hence thesis by XTUPLE_0:def 12; end; then A10: dom f = bool the carrier' of C by A7,TARSKI:2; rng f c= bool the carrier of C proof let y be object; assume y in rng f; then consider x being object such that A11: [x,y] in f by XTUPLE_0:def 13; consider A being Subset of the carrier' of C such that A12: [x,y] = [A,{o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}] by A11; A13: {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a} c= the carrier of C proof let u be object; assume u in {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}; then ex u9 being Object of C st u9 = u & for a being Attribute of C st a in A holds u9 is-connected-with a; hence thesis; end; y = [x,y]`2 .=[A,{o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}]`2 by A12 .= {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}; hence thesis by A13; end; then reconsider f as Function of bool the carrier' of C,bool the carrier of C by A10,FUNCT_2:def 1,RELSET_1:4; take f; for A being Subset of the carrier' of C holds f.A = {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a} proof let A be Subset of the carrier' of C; consider y being object such that A14: [A,y] in f by A10,XTUPLE_0:def 12; consider A9 being Subset of the carrier' of C such that A15: [A,y] = [A9,{o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a}] by A14; A16: y = [A,y]`2 .=[A9,{o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a}]`2 by A15 .= {o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a}; A = [A,y]`1 .=[A9,{o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a}]`1 by A15 .= A9; hence thesis by A10,A14,A16,FUNCT_1:def 2; end; hence thesis; end; uniqueness proof let F1,F2 be Function of bool the carrier' of C,bool the carrier of C; assume A17: for A being Subset of the carrier' of C holds F1.A = {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}; assume A18: for A being Subset of the carrier' of C holds F2.A = {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}; A19: for A being object st A in bool the carrier' of C holds F1.A = F2.A proof let A be object; assume A in bool the carrier' of C; then reconsider A as Subset of the carrier' of C; F1.A = {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a} by A17 .= F2.A by A18; hence thesis; end; dom F1 = bool the carrier' of C & dom F2 = bool the carrier' of C by FUNCT_2:def 1; hence thesis by A19,FUNCT_1:2; end; end; theorem for C being FormalContext for o being Object of C holds ( ObjectDerivation(C)).({o}) = {a where a is Attribute of C : o is-connected-with a} proof let C be FormalContext; let o be Object of C; {o} c= the carrier of C proof let x be object; assume x in {o}; then x = o by TARSKI:def 1; hence thesis; end; then reconsider t = {o} as Subset of the carrier of C; A1: for x being object holds x in {a where a is Attribute of C : for o9 being Object of C st o9 in t holds o9 is-connected-with a} implies x in {a where a is Attribute of C : o is-connected-with a} proof set o9 = the Element of t; let x be object; reconsider o9 as Object of C by TARSKI:def 1; A2: o9 = o by TARSKI:def 1; assume x in {a where a is Attribute of C : for o9 being Object of C st o9 in t holds o9 is-connected-with a}; then A3: ex x9 being Attribute of C st x9 = x & for o9 being Object of C st o9 in t holds o9 is-connected-with x9; then reconsider x as Attribute of C; o9 is-connected-with x by A3; hence thesis by A2; end; A4: for x being object holds x in {a where a is Attribute of C : o is-connected-with a} implies x in {a where a is Attribute of C : for o9 being Object of C st o9 in t holds o9 is-connected-with a} proof let x be object; assume x in {a where a is Attribute of C : o is-connected-with a}; then A5: ex x9 being Attribute of C st x9 = x & o is-connected-with x9; then reconsider x as Attribute of C; for o9 being Object of C st o9 in t holds o9 is-connected-with x by A5, TARSKI:def 1; hence thesis; end; (ObjectDerivation(C)).t = {a where a is Attribute of C : for o9 being Object of C st o9 in t holds o9 is-connected-with a} by Def2; hence thesis by A1,A4,TARSKI:2; end; theorem for C being FormalContext for a being Attribute of C holds ( AttributeDerivation(C)).({a}) = {o where o is Object of C : o is-connected-with a} proof let C be FormalContext; let a be Attribute of C; {a} c= the carrier' of C proof let x be object; assume x in {a}; then x = a by TARSKI:def 1; hence thesis; end; then reconsider t = {a} as Subset of the carrier' of C; A1: for x being object holds x in {o where o is Object of C : for a9 being Attribute of C st a9 in t holds o is-connected-with a9} implies x in {o where o is Object of C : o is-connected-with a} proof set a9 = the Element of t; let x be object; reconsider a9 as Attribute of C by TARSKI:def 1; A2: a9 = a by TARSKI:def 1; assume x in {o where o is Object of C : for a9 being Attribute of C st a9 in t holds o is-connected-with a9}; then A3: ex x9 being Object of C st x9 = x & for a9 being Attribute of C st a9 in t holds x9 is-connected-with a9; then reconsider x as Object of C; x is-connected-with a9 by A3; hence thesis by A2; end; A4: for x being object holds x in {o where o is Object of C : o is-connected-with a} implies x in {o where o is Object of C : for a9 being Attribute of C st a9 in t holds o is-connected-with a9} proof let x be object; assume x in {o where o is Object of C : o is-connected-with a}; then A5: ex x9 being Object of C st x9 = x & x9 is-connected-with a; then reconsider x as Object of C; for a9 being Attribute of C st a9 in t holds x is-connected-with a9 by A5,TARSKI:def 1; hence thesis; end; (AttributeDerivation(C)).t = {o where o is Object of C : for a9 being Attribute of C st a9 in t holds o is-connected-with a9} by Def3; hence thesis by A1,A4,TARSKI:2; end; theorem Th3: for C being FormalContext for O1,O2 being Subset of the carrier of C holds O1 c= O2 implies (ObjectDerivation(C)).O2 c= (ObjectDerivation(C)). O1 proof let C be FormalContext; let O1,O2 be Subset of the carrier of C; assume A1: O1 c= O2; let x be object; assume x in (ObjectDerivation(C)).O2; then x in {a where a is Attribute of C : for o being Object of C st o in O2 holds o is-connected-with a} by Def2; then consider x9 being Attribute of C such that A2: x9 = x and A3: for o being Object of C st o in O2 holds o is-connected-with x9; for o being Object of C st o in O1 holds o is-connected-with x9 by A1,A3; then x in {a where a is Attribute of C : for o being Object of C st o in O1 holds o is-connected-with a} by A2; hence thesis by Def2; end; theorem Th4: for C being FormalContext for A1,A2 being Subset of the carrier' of C holds A1 c= A2 implies (AttributeDerivation(C)).A2 c= (AttributeDerivation (C)).A1 proof let C be FormalContext; let A1,A2 be Subset of the carrier' of C; assume A1: A1 c= A2; let x be object; assume x in (AttributeDerivation(C)).A2; then x in {o where o is Object of C : for a being Attribute of C st a in A2 holds o is-connected-with a} by Def3; then consider x9 being Object of C such that A2: x9 = x and A3: for a being Attribute of C st a in A2 holds x9 is-connected-with a; for a being Attribute of C st a in A1 holds x9 is-connected-with a by A1,A3; then x in {o where o is Object of C : for a being Attribute of C st a in A1 holds o is-connected-with a} by A2; hence thesis by Def3; end; theorem Th5: for C being FormalContext for O being Subset of the carrier of C holds O c= (AttributeDerivation(C)).((ObjectDerivation(C)).O) proof let C be FormalContext; let O be Subset of the carrier of C; set A = {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}; for x being object holds x in A implies x in the carrier' of C proof let x be object; assume x in A; then 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; hence thesis; end; then reconsider A as Subset of the carrier' of C by TARSKI:def 3; let x be object; assume A1: x in O; then reconsider x as Object of C; A2: for a being Attribute of C st a in A holds x is-connected-with a proof let a be Attribute of C; assume a in A; then ex a9 being Attribute of C st a9 = a & for o being Object of C st o in O holds o is-connected-with a9; hence thesis by A1; end; (AttributeDerivation(C)).A = {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a} by Def3; then x in (AttributeDerivation(C)).A by A2; hence thesis by Def2; end; theorem Th6: for C being FormalContext for A being Subset of the carrier' of C holds A c= (ObjectDerivation(C)).((AttributeDerivation(C)).A) proof let C be FormalContext; let A be Subset of the carrier' of C; set O = {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}; for x being object holds x in O implies x in the carrier of C proof let x be object; assume x in O; then 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; hence thesis; end; then reconsider O as Subset of the carrier of C by TARSKI:def 3; let x be object; assume A1: x in A; then reconsider x as Attribute of C; A2: for o being Object of C st o in O holds o is-connected-with x proof let o be Object of C; assume o in O; then ex o9 being Object of C st o9 = o & for a being Attribute of C st a in A holds o9 is-connected-with a; hence thesis by A1; 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} by Def2; then x in (ObjectDerivation(C)).O by A2; hence thesis by Def3; end; theorem Th7: for C being FormalContext for O being Subset of the carrier of C holds (ObjectDerivation(C)).O = (ObjectDerivation(C)).((AttributeDerivation(C)) .((ObjectDerivation(C)).O)) proof let C be FormalContext; let O be Subset of the carrier of C; set A = {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}; set O9 = {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}; set A9 = {a where a is Attribute of C : for o being Object of C st o in O9 holds o is-connected-with a}; A1: for x being object holds x in A9 implies x in A proof let x be object; assume x in A9; then A2: ex x9 being Attribute of C st x9 = x & for o being Object of C st o in O9 holds o is-connected-with x9; then reconsider x as Attribute of C; for o being Object of C st o in O holds o is-connected-with x proof let o be Object of C; assume A3: o in O; now per cases; case o in O9; hence thesis by A2; end; case not o in O9; then consider a being Attribute of C such that A4: a in A and A5: not o is-connected-with a; ex a9 being Attribute of C st a9 = a & for o being Object of C st o in O holds o is-connected-with a9 by A4; hence thesis by A3,A5; end; end; hence thesis; end; hence thesis; end; for x being object holds x in A implies x in A9 proof let x be object; assume A6: x in A; then 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; then reconsider x as Attribute of C; for o being Object of C st o in O9 holds o is-connected-with x proof let o be Object of C; assume o in O9; then ex o9 being Object of C st o9 = o & for a being Attribute of C st a in A holds o9 is-connected-with a; hence thesis by A6; end; hence thesis; end; then A7: A = A9 by A1,TARSKI:2; A c= the carrier' of C proof let x be object; assume x in A; then 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; hence thesis; end; then reconsider A as Subset of the carrier' of C; O9 c= the carrier of C proof let x be object; assume x in O9; then 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; hence thesis; end; then reconsider O9 as Subset of the carrier of C; A = (ObjectDerivation(C)).O & O9 = (AttributeDerivation(C)).A by Def2,Def3; hence thesis by A7,Def2; end; theorem Th8: for C being FormalContext for A being Subset of the carrier' of C holds (AttributeDerivation(C)).A = (AttributeDerivation(C)).((ObjectDerivation( C)).((AttributeDerivation(C)).A)) proof let C be FormalContext; let A be Subset of the carrier' of C; set O = {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}; set A9 = {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}; set O9 = {o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a}; A1: for x being object holds x in O9 implies x in O proof let x be object; assume x in O9; then A2: ex x9 being Object of C st x9 = x & for a being Attribute of C st a in A9 holds x9 is-connected-with a; then reconsider x as Object of C; for a being Attribute of C st a in A holds x is-connected-with a proof let a be Attribute of C; assume A3: a in A; now per cases; case a in A9; hence thesis by A2; end; case not a in A9; then consider o being Object of C such that A4: o in O and A5: not o is-connected-with a; ex o9 being Object of C st o9 = o & for a being Attribute of C st a in A holds o9 is-connected-with a by A4; hence thesis by A3,A5; end; end; hence thesis; end; hence thesis; end; for x being object holds x in O implies x in O9 proof let x be object; assume A6: x in O; then 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; then reconsider x as Object of C; for a being Attribute of C st a in A9 holds x is-connected-with a proof let a be Attribute of C; assume a in A9; then ex a9 being Attribute of C st a9 = a & for o being Object of C st o in O holds o is-connected-with a9; hence thesis by A6; end; hence thesis; end; then A7: O = O9 by A1,TARSKI:2; O c= the carrier of C proof let x be object; assume x in O; then 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; hence thesis; end; then reconsider O as Subset of the carrier of C; A9 c= the carrier' of C proof let x be object; assume x in A9; then 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; hence thesis; end; then reconsider A9 as Subset of the carrier' of C; O = (AttributeDerivation(C)).A & A9 = (ObjectDerivation(C)).O by Def2,Def3; hence thesis by A7,Def3; end; theorem Th9: for C being FormalContext for O being Subset of the carrier of C for A being Subset of the carrier' of C holds O c= (AttributeDerivation(C)).A iff [:O,A:] c= the Information of C proof let C be FormalContext; let O be Subset of the carrier of C; let A be Subset of the carrier' of C; A1: [:O,A:] c= the Information of C implies O c= (AttributeDerivation(C)).A proof assume A2: [:O,A:] c= the Information of C; let x be object; assume A3: x in O; then reconsider x as Object of C; for a being Attribute of C st a in A holds x is-connected-with a proof let a be Attribute of C; consider z being set such that A4: z = [x,a]; assume a in A; then z in [:O,A:] by A3,A4,ZFMISC_1:def 2; hence thesis by A2,A4; end; then x in {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a}; hence thesis by Def3; end; O c= (AttributeDerivation(C)).A implies [:O,A:] c= the Information of C proof assume O c= (AttributeDerivation(C)).A; then A5: O c= {o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a} by Def3; let z be object; assume z in [:O,A:]; then consider x,y being object such that A6: x in O and A7: y in A and A8: z = [x,y] by ZFMISC_1:def 2; reconsider y as Attribute of C by A7; reconsider x as Object of C by A6; 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 A5,A6; then 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; then x is-connected-with y by A7; hence thesis by A8; end; hence thesis by A1; end; theorem Th10: for C being FormalContext for O being Subset of the carrier of C for A being Subset of the carrier' of C holds A c= (ObjectDerivation(C)).O iff [:O,A:] c= the Information of C proof let C be FormalContext; let O be Subset of the carrier of C; let A be Subset of the carrier' of C; A1: [:O,A:] c= the Information of C implies A c= (ObjectDerivation(C)).O proof assume A2: [:O,A:] c= the Information of C; let x be object; assume A3: x in A; then reconsider x as Attribute of C; for o being Object of C st o in O holds o is-connected-with x proof let o be Object of C; consider z being set such that A4: z = [o,x]; assume o in O; then z in [:O,A:] by A3,A4,ZFMISC_1:def 2; hence thesis by A2,A4; end; then x in {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a}; hence thesis by Def2; end; A c= (ObjectDerivation(C)).O implies [:O,A:] c= the Information of C proof assume A c= (ObjectDerivation(C)).O; then A5: A c= {a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a} by Def2; let z be object; assume z in [:O,A:]; then consider x,y being object such that A6: x in O and A7: y in A and A8: z = [x,y] by ZFMISC_1:def 2; reconsider y as Attribute of C by A7; reconsider x as Object of C by A6; y 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 A5,A7; then ex y9 being Attribute of C st y9 = y & for o being Object of C st o in O holds o is-connected-with y9; then x is-connected-with y by A6; hence thesis by A8; end; hence thesis by A1; end; theorem for C being FormalContext for O being Subset of the carrier of C for A being Subset of the carrier' of C holds O c= (AttributeDerivation(C)).A iff A c= (ObjectDerivation(C)).O proof let C be FormalContext; let O be Subset of the carrier of C; let A be Subset of the carrier' of C; O c= (AttributeDerivation(C)).A iff [:O,A:] c= the Information of C by Th9; hence thesis by Th10; end; definition let C be FormalContext; func phi(C) -> Function of BoolePoset the carrier of C, BoolePoset the carrier' of C equals ObjectDerivation(C); coherence proof A1: rng(ObjectDerivation(C)) c= the carrier of BoolePoset the carrier' of C proof let x be object; assume x in rng(ObjectDerivation(C)); then x in bool the carrier' of C; then A2: x in the carrier of BooleLatt the carrier' of C by LATTICE3:def 1; LattPOSet BooleLatt the carrier' of C = RelStr (#the carrier of BooleLatt the carrier' of C, LattRel BooleLatt the carrier' of C#) by LATTICE3:def 2; hence thesis by A2,YELLOW_1:def 2; end; A3: LattPOSet BooleLatt the carrier of C = RelStr (#the carrier of BooleLatt the carrier of C, LattRel BooleLatt the carrier of C#) by LATTICE3:def 2; A4: for x being object holds x in the carrier of BoolePoset the carrier of C implies x in dom(ObjectDerivation(C)) proof let x be object; assume x in the carrier of BoolePoset the carrier of C; then x in the carrier of LattPOSet BooleLatt the carrier of C by YELLOW_1:def 2; then x in bool the carrier of C by A3,LATTICE3:def 1; hence thesis by FUNCT_2:def 1; end; for x being object holds x in dom(ObjectDerivation(C)) implies x in the carrier of BoolePoset the carrier of C proof let x be object; assume x in dom(ObjectDerivation(C)); then x in bool the carrier of C; then x in the carrier of BooleLatt the carrier of C by LATTICE3:def 1; hence thesis by A3,YELLOW_1:def 2; end; then dom(ObjectDerivation(C)) = the carrier of BoolePoset the carrier of C by A4,TARSKI:2; then reconsider g = ObjectDerivation(C) as Function of the carrier of BoolePoset the carrier of C, the carrier of BoolePoset the carrier' of C by A1,FUNCT_2:def 1,RELSET_1:4; g is Function of BoolePoset the carrier of C, BoolePoset the carrier' of C; hence thesis; end; end; definition let C be FormalContext; func psi(C) -> Function of BoolePoset the carrier' of C, BoolePoset the carrier of C equals AttributeDerivation(C); coherence proof A1: rng(AttributeDerivation(C)) c= the carrier of BoolePoset(the carrier of C) proof let x be object; assume x in rng(AttributeDerivation(C)); then x in bool the carrier of C; then A2: x in the carrier of (BooleLatt the carrier of C) by LATTICE3:def 1; LattPOSet BooleLatt the carrier of C = RelStr (#the carrier of BooleLatt the carrier of C, LattRel BooleLatt the carrier of C#) by LATTICE3:def 2; hence thesis by A2,YELLOW_1:def 2; end; A3: LattPOSet BooleLatt the carrier' of C = RelStr (#the carrier of BooleLatt the carrier' of C, LattRel BooleLatt the carrier' of C#) by LATTICE3:def 2; A4: for x being object holds x in the carrier of BoolePoset(the carrier' of C ) implies x in dom(AttributeDerivation(C)) proof let x be object; assume x in the carrier of BoolePoset the carrier' of C; then x in the carrier of LattPOSet BooleLatt the carrier' of C by YELLOW_1:def 2; then x in bool the carrier' of C by A3,LATTICE3:def 1; hence thesis by FUNCT_2:def 1; end; for x being object holds x in dom(AttributeDerivation(C)) implies x in the carrier of BoolePoset the carrier' of C proof let x be object; assume x in dom(AttributeDerivation(C)); then x in bool the carrier' of C; then x in the carrier of BooleLatt the carrier' of C by LATTICE3:def 1; hence thesis by A3,YELLOW_1:def 2; end; then dom(AttributeDerivation(C)) = the carrier of BoolePoset the carrier' of C by A4,TARSKI:2; hence thesis by A1,FUNCT_2:def 1,RELSET_1:4; end; end; definition let P,R be non empty RelStr; let Con be Connection of P,R; attr Con is co-Galois means ex f being Function of P,R, g being Function of R,P st (Con = [f,g] & f is antitone & g is antitone & for p1,p2 being Element of P, r1,r2 being Element of R holds p1 <= g.(f.p1) & r1 <= f.(g. r1)); end; theorem Th12: for P,R being non empty Poset for Con being Connection of P,R for f being Function of P,R, g being Function of R,P st Con = [f,g] holds Con is co-Galois iff for p being Element of P, r being Element of R holds p <= g.r iff r <= f.p proof let P,R be non empty Poset; let Con be Connection of P,R; let f be Function of P,R, g be Function of R,P; assume A1: Con = [f,g]; A2: now assume A3: for p being Element of P, r being Element of R holds p <= g.r iff r <= f.p; for p1,p2 being Element of P st p1 <= p2 for r1,r2 being Element of R st r1 = f.p1 & r2 = f.p2 holds r1 >= r2 proof let p1,p2 be Element of P; assume A4: p1 <= p2; let r1,r2 be Element of R; assume A5: r1 = f.p1 & r2 = f.p2; p2 <= g.(f.p2) by A3; then p1 <= g.(f.p2) by A4,ORDERS_2:3; hence thesis by A3,A5; end; then A6: f is antitone by WAYBEL_0:def 5; for r1,r2 being Element of R st r1 <= r2 for p1,p2 being Element of P st p1 = g.r1 & p2 = g.r2 holds p1 >= p2 proof let r1,r2 be Element of R; assume A7: r1 <= r2; let p1,p2 be Element of P; assume A8: p1 = g.r1 & p2 = g.r2; r2 <= f.(g.r2) by A3; then r1 <= f.(g.r2) by A7,ORDERS_2:3; hence thesis by A3,A8; end; then A9: g is antitone by WAYBEL_0:def 5; for p1,p2 being Element of P, r1,r2 being Element of R holds p1 <= g. (f.p1) & r1 <= f.(g.r1) by A3; hence Con is co-Galois by A1,A6,A9; end; now assume Con is co-Galois; then consider f9 being Function of P,R, g9 being Function of R,P such that A10: Con = [f9,g9] and A11: f9 is antitone and A12: g9 is antitone and A13: for p1,p2 being Element of P, r1,r2 being Element of R holds p1 <= g9.(f9.p1) & r1 <= f9.(g9.r1); A14: g = [f,g]`2 .= Con`2 by A1 .= [f9,g9]`2 by A10 .= g9; A15: f = [f,g]`1 .= Con`1 by A1 .= [f9,g9]`1 by A10 .= f9; A16: for p being Element of P, r being Element of R holds r <= f.p implies p <= g.r proof let p be Element of P, r be Element of R; assume r <= f.p; then A17: g.r >= g.(f.p) by A12,A14,WAYBEL_0:def 5; p <= g.(f.p) by A13,A15,A14; hence thesis by A17,ORDERS_2:3; end; for p being Element of P, r being Element of R holds p <= g.r implies r <= f.p proof let p be Element of P, r be Element of R; assume p <= g.r; then A18: f.p >= f.(g.r) by A11,A15,WAYBEL_0:def 5; r <= f.(g.r) by A13,A15,A14; hence thesis by A18,ORDERS_2:3; end; hence for p being Element of P, r being Element of R holds p <= g.r iff r <= f.p by A16; end; hence thesis by A2; end; theorem for P,R being non empty Poset for Con being Connection of P,R st Con is co-Galois for f being Function of P,R, g being Function of R,P st Con = [f,g ] holds f = f * (g * f) & g = g * (f * g) proof let P,R be non empty Poset; let Con be Connection of P,R; assume Con is co-Galois; then consider f9 being Function of P,R, g9 being Function of R,P such that A1: Con = [f9,g9] and A2: f9 is antitone and A3: g9 is antitone and A4: for p1,p2 being Element of P, r1,r2 being Element of R holds p1 <= g9.(f9.p1) & r1 <= f9.(g9.r1); let f be Function of P,R, g be Function of R,P; assume A5: Con = [f,g]; A6: f = [f,g]`1 .= Con`1 by A5 .= [f9,g9]`1 by A1 .= f9; A7: g = [f,g]`2 .= Con`2 by A5 .= [f9,g9]`2 by A1 .= g9; A8: dom g = the carrier of R by FUNCT_2:def 1; A9: dom f = the carrier of P by FUNCT_2:def 1; A10: for x being object st x in the carrier of P holds f.x =(f*(g*f)).x proof let x be object; assume x in the carrier of P; then reconsider x as Element of P; x <= g.(f.x) by A4,A6,A7; then A11: f.x >= f.(g.(f.x)) by A2,A6,WAYBEL_0:def 5; f.x <= f.(g.(f.x)) by A4,A6,A7; then f.x = f.(g.(f.x)) by A11,ORDERS_2:2; then A12: f.x = f.((g*f).x) by A9,FUNCT_1:13; f.x is Element of R; then x in dom (g*f) by A9,A8,FUNCT_1:11; hence thesis by A12,FUNCT_1:13; end; A13: for x being object st x in the carrier of R holds g.x =(g*(f*g)).x proof let x be object; assume x in the carrier of R; then reconsider x as Element of R; x <= f.(g.x) by A4,A6,A7; then A14: g.x >= g.(f.(g.x)) by A3,A7,WAYBEL_0:def 5; g.x <= g.(f.(g.x)) by A4,A6,A7; then g.x = g.(f.(g.x)) by A14,ORDERS_2:2; then A15: g.x = g.((f*g).x) by A8,FUNCT_1:13; g.x is Element of P; then x in dom (f*g) by A9,A8,FUNCT_1:11; hence thesis by A15,FUNCT_1:13; end; dom (f*(g*f)) = the carrier of P & dom (g*(f*g)) = the carrier of R by FUNCT_2:def 1; hence thesis by A9,A8,A10,A13,FUNCT_1:2; end; theorem for C being FormalContext holds [phi(C),psi(C)] is co-Galois proof let C be FormalContext; A1: LattPOSet BooleLatt the carrier' of C = RelStr (#the carrier of BooleLatt the carrier' of C, LattRel BooleLatt the carrier' of C#) by LATTICE3:def 2; A2: LattPOSet BooleLatt the carrier of C = RelStr (#the carrier of BooleLatt the carrier of C, LattRel BooleLatt the carrier of C#) by LATTICE3:def 2; A3: for x being Element of BoolePoset the carrier of C, y being Element of BoolePoset the carrier' of C st y <= (phi(C)).x holds x <= (psi(C)).y proof let x be Element of BoolePoset the carrier of C, y be Element of BoolePoset the carrier' of C; assume y <= (phi(C)).x; then [y,(phi(C)).x] in the InternalRel of (BoolePoset the carrier' of C) by ORDERS_2:def 5; then A4: [y,(phi(C)).x] in LattRel (BooleLatt the carrier' of C) by A1, YELLOW_1:def 2; reconsider x9 = (phi(C)).x as Element of (BooleLatt the carrier' of C) by A1,YELLOW_1:def 2; reconsider x as Element of BooleLatt the carrier of C by A2,YELLOW_1:def 2; reconsider x as Subset of the carrier of C by LATTICE3:def 1; reconsider y as Element of (BooleLatt the carrier' of C) by A1, YELLOW_1:def 2; y [= x9 by A4,FILTER_1:31; then A5: y "\/" x9 = x9 by LATTICES:def 3; reconsider x9 as Subset of the carrier' of C by LATTICE3:def 1; reconsider y as Subset of the carrier' of C by LATTICE3:def 1; for z being object holds z in y implies z in x9 by A5,XBOOLE_0:def 3; then y c= x9; then A6: (AttributeDerivation(C)).x9 c= (AttributeDerivation(C)).y by Th4; reconsider y as Element of BoolePoset the carrier' of C; reconsider y9 = (psi(C)).y as Element of (BooleLatt the carrier of C) by A2 ,YELLOW_1:def 2; reconsider y9 as Subset of the carrier of C by LATTICE3:def 1; reconsider y9 as Element of (BooleLatt the carrier of C); A7: x c= (AttributeDerivation(C)).((ObjectDerivation(C)).x) by Th5; reconsider x as Subset of the carrier of C; reconsider x as Element of (BooleLatt the carrier of C); x "\/" y9 = y9 by A6,A7,XBOOLE_1:1,12; then x [= y9 by LATTICES:def 3; then [x,(psi(C)).y] in LattRel (BooleLatt the carrier of C) by FILTER_1:31; then [x,(psi(C)).y] in the InternalRel of (BoolePoset the carrier of C) by A2, YELLOW_1:def 2; hence thesis by ORDERS_2:def 5; end; for x being Element of BoolePoset the carrier of C, y being Element of BoolePoset the carrier' of C st x <= (psi(C)).y holds y <= (phi(C)).x proof let x be Element of BoolePoset the carrier of C, y be Element of BoolePoset the carrier' of C; assume x <= (psi(C)).y; then [x,(psi(C)).y] in the InternalRel of (BoolePoset the carrier of C) by ORDERS_2:def 5; then A8: [x,(psi(C)).y] in LattRel (BooleLatt the carrier of C) by A2,YELLOW_1:def 2 ; reconsider y9 = (psi(C)).y as Element of (BooleLatt the carrier of C) by A2 ,YELLOW_1:def 2; reconsider y as Element of (BooleLatt the carrier' of C) by A1, YELLOW_1:def 2; reconsider y as Subset of the carrier' of C by LATTICE3:def 1; reconsider x as Element of (BooleLatt the carrier of C) by A2, YELLOW_1:def 2; x [= y9 by A8,FILTER_1:31; then A9: x "\/" y9 = y9 by LATTICES:def 3; reconsider y9 as Subset of the carrier of C by LATTICE3:def 1; reconsider x as Subset of the carrier of C by LATTICE3:def 1; for z being object holds z in x implies z in y9 by A9,XBOOLE_0:def 3; then A10: x c= y9; reconsider x,y9 as Subset of the carrier of C; A11: (ObjectDerivation(C)).y9 c= (ObjectDerivation(C)).x by A10,Th3; reconsider x as Element of BoolePoset the carrier of C; reconsider x9 = (phi(C)).x as Element of (BooleLatt the carrier' of C) by A1,YELLOW_1:def 2; reconsider x9 as Subset of the carrier' of C by LATTICE3:def 1; reconsider x9 as Element of (BooleLatt the carrier' of C); A12: y c= (ObjectDerivation(C)).((AttributeDerivation(C)).y) by Th6; reconsider y as Element of (BooleLatt the carrier' of C); y "\/" x9 = x9 by A11,A12,XBOOLE_1:1,12; then y [= x9 by LATTICES:def 3; then [y,(phi(C)).x] in LattRel (BooleLatt the carrier' of C) by FILTER_1:31 ; then [y,(phi(C)).x] in the InternalRel of (BoolePoset the carrier' of C) by A1,YELLOW_1:def 2; hence thesis by ORDERS_2:def 5; end; hence thesis by A3,Th12; end; theorem Th15: for C being FormalContext for O1,O2 being Subset of the carrier of C holds (ObjectDerivation(C)).(O1 \/ O2) = ((ObjectDerivation(C)).O1) /\ (( ObjectDerivation(C)).O2) proof let C be FormalContext; let O1,O2 be Subset of the carrier of C; reconsider O9 = O1 \/ O2 as Subset of the carrier of C; A1: for x being object holds x in (ObjectDerivation(C)).O1 /\ ( ObjectDerivation( C ) ) . O2 implies x in (ObjectDerivation(C)).O9 proof let x be object; assume A2: x in (ObjectDerivation(C)).O1 /\ (ObjectDerivation(C)).O2; then x in (ObjectDerivation(C)).O1 by XBOOLE_0:def 4; then x in {a where a is Attribute of C : for o being Object of C st o in O1 holds o is-connected-with a} by Def2; then A3: ex x1 being Attribute of C st x1 = x & for o being Object of C st o in O1 holds o is-connected-with x1; x in (ObjectDerivation(C)).O2 by A2,XBOOLE_0:def 4; then x in {a where a is Attribute of C : for o being Object of C st o in O2 holds o is-connected-with a } by Def2; then A4: ex x2 being Attribute of C st x2 = x & for o being Object of C st o in O2 holds o is-connected-with x2; then reconsider x as Attribute of C; for o being Object of C st o in O1 \/ O2 holds o is-connected-with x proof let o be Object of C; assume A5: o in (O1 \/ O2); now per cases by A5,XBOOLE_0:def 3; case o in O1; hence thesis by A3; end; case o in O2; hence thesis by A4; end; end; hence thesis; end; then x in {a where a is Attribute of C : for o being Object of C st o in O9 holds o is-connected-with a}; hence thesis by Def2; end; for x being object holds x in (ObjectDerivation(C)).(O1 \/ O2) implies x in (ObjectDerivation(C)).O1 /\ (ObjectDerivation(C)).O2 proof let x be object; assume x in (ObjectDerivation(C)).(O1 \/ O2); then x in {a where a is Attribute of C : for o being Object of C st o in O9 holds o is-connected-with a} by Def2; then A6: ex x9 being Attribute of C st x9 = x & for o being Object of C st o in O9 holds o is-connected-with x9; then reconsider x as Attribute of C; for o being Object of C st o in O2 holds o is-connected-with x proof let o be Object of C; assume o in O2; then o in O9 by XBOOLE_0:def 3; hence thesis by A6; end; then x in {a where a is Attribute of C : for o being Object of C st o in O2 holds o is-connected-with a}; then A7: x in (ObjectDerivation(C)).O2 by Def2; for o being Object of C st o in O1 holds o is-connected-with x proof let o be Object of C; assume o in O1; then o in O9 by XBOOLE_0:def 3; hence thesis by A6; end; then x in {a where a is Attribute of C : for o being Object of C st o in O1 holds o is-connected-with a}; then x in (ObjectDerivation(C)).O1 by Def2; hence thesis by A7,XBOOLE_0:def 4; end; hence thesis by A1,TARSKI:2; end; theorem Th16: for C being FormalContext for A1,A2 being Subset of the carrier' of C holds (AttributeDerivation(C)).(A1 \/ A2) = ((AttributeDerivation(C)).A1) /\ ((AttributeDerivation(C)).A2) proof let C be FormalContext; let A1,A2 be Subset of the carrier' of C; reconsider A9 = A1 \/ A2 as Subset of the carrier' of C; A1: for x being object holds x in (AttributeDerivation(C)).A1 /\ ( AttributeDerivation(C)).A2 implies x in (AttributeDerivation(C)).A9 proof let x be object; assume A2: x in (AttributeDerivation(C)).A1 /\ (AttributeDerivation(C)).A2; then x in (AttributeDerivation(C)).A1 by XBOOLE_0:def 4; then x in {o where o is Object of C : for a being Attribute of C st a in A1 holds o is-connected-with a} by Def3; then A3: ex x1 being Object of C st x1 = x & for a being Attribute of C st a in A1 holds x1 is-connected-with a; x in (AttributeDerivation(C)).A2 by A2,XBOOLE_0:def 4; then x in {o where o is Object of C : for a being Attribute of C st a in A2 holds o is-connected-with a} by Def3; then A4: ex x2 being Object of C st x2 = x & for a being Attribute of C st a in A2 holds x2 is-connected-with a; then reconsider x as Object of C; for a being Attribute of C st a in A1 \/ A2 holds x is-connected-with a proof let a be Attribute of C; assume A5: a in (A1 \/ A2); now per cases by A5,XBOOLE_0:def 3; case a in A1; hence thesis by A3; end; case a in A2; hence thesis by A4; end; end; hence thesis; end; then x in {o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a}; hence thesis by Def3; end; for x being object holds x in (AttributeDerivation(C)).(A1 \/ A2) implies x in (AttributeDerivation(C)).A1 /\ (AttributeDerivation(C)).A2 proof let x be object; assume x in (AttributeDerivation(C)).(A1 \/ A2); then x in {o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a} by Def3; then A6: ex x9 being Object of C st x9 = x & for a being Attribute of C st a in A9 holds x9 is-connected-with a; then reconsider x as Object of C; for a being Attribute of C st a in A2 holds x is-connected-with a proof let a be Attribute of C; assume a in A2; then a in A9 by XBOOLE_0:def 3; hence thesis by A6; end; then x in {o where o is Object of C : for a being Attribute of C st a in A2 holds o is-connected-with a}; then A7: x in (AttributeDerivation(C)).A2 by Def3; for a being Attribute of C st a in A1 holds x is-connected-with a proof let a be Attribute of C; assume a in A1; then a in A9 by XBOOLE_0:def 3; hence thesis by A6; end; then x in {o where o is Object of C : for a being Attribute of C st a in A1 holds o is-connected-with a}; then x in (AttributeDerivation(C)).A1 by Def3; hence thesis by A7,XBOOLE_0:def 4; end; hence thesis by A1,TARSKI:2; end; theorem Th17: for C being FormalContext holds (ObjectDerivation(C)).{} = the carrier' of C proof let C be FormalContext; reconsider e = {} as Subset of the carrier of C by XBOOLE_1:2; set A = {a where a is Attribute of C : for o being Object of C st o in e holds o is-connected-with a}; A1: for x being object holds x in A implies x in the carrier' of C proof let x be object; assume x in A; then ex x9 being Attribute of C st x9 = x & for o being Object of C st o in e holds o is-connected-with x9; hence thesis; end; A2: for x being object holds x in the carrier' of C implies x in A proof let x be object; assume x in the carrier' of C; then reconsider x as Attribute of C; for o being Object of C st o in e holds o is-connected-with x; hence thesis; end; (ObjectDerivation(C)).e = {a where a is Attribute of C : for o being Object of C st o in e holds o is-connected-with a} by Def2; hence thesis by A1,A2,TARSKI:2; end; theorem Th18: for C being FormalContext holds (AttributeDerivation(C)).{} = the carrier of C proof let C be FormalContext; reconsider e = {} as Subset of the carrier' of C by XBOOLE_1:2; set O = {o where o is Object of C : for a being Attribute of C st a in e holds o is-connected-with a}; A1: for x being object holds x in O implies x in the carrier of C proof let x be object; assume x in O; then ex x9 being Object of C st x9 = x & for a being Attribute of C st a in e holds x9 is-connected-with a; hence thesis; end; A2: for x being object holds x in the carrier of C implies x in O proof let x be object; assume x in the carrier of C; then reconsider x as Object of C; for a being Attribute of C st a in e holds x is-connected-with a; hence thesis; end; (AttributeDerivation(C)).e = {o where o is Object of C : for a being Attribute of C st a in e holds o is-connected-with a} by Def3; hence thesis by A1,A2,TARSKI:2; end; begin :: Formal Concepts definition let C be 2-sorted; struct ConceptStr over C (# Extent -> Subset of the carrier of C, Intent -> Subset of the carrier' of C #); end; definition let C be 2-sorted; let CP be ConceptStr over C; attr CP is empty means :Def7: the Extent of CP is empty & the Intent of CP is empty; attr CP is quasi-empty means :Def8: the Extent of CP is empty or the Intent of CP is empty; end; registration let C be non empty non void 2-sorted; cluster strict non empty for ConceptStr over C; existence proof set A = the non empty Subset of the carrier' of C; set O = the non empty Subset of the carrier of C; ConceptStr(#O,A#) is non empty; hence thesis; end; cluster strict quasi-empty for ConceptStr over C; existence proof reconsider A = {} as Subset of the carrier' of C by XBOOLE_1:2; reconsider O = {} as Subset of the carrier of C by XBOOLE_1:2; ConceptStr(#O,A#) is quasi-empty; hence thesis; end; end; registration let C be empty void 2-sorted; cluster -> empty for ConceptStr over C; coherence; end; Lm1: for C being FormalContext for CS being ConceptStr over C st ( ObjectDerivation(C)).(the Extent of CS) = the Intent of CS holds CS is non empty proof let C be FormalContext; let CS be ConceptStr over C; assume A1: (ObjectDerivation(C)).(the Extent of CS) = the Intent of CS; now per cases; case the Extent of CS is empty; then the Intent of CS = the carrier' of C by A1,Th17; hence thesis; end; case the Extent of CS is non empty; hence thesis; end; end; hence thesis; end; definition let C be FormalContext; let CP be ConceptStr over C; attr CP is concept-like means :Def9: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP & (AttributeDerivation(C)).(the Intent of CP) = the Extent of CP; end; registration let C be FormalContext; cluster concept-like non empty for ConceptStr over C; existence proof set o = the Object of C; set A = (ObjectDerivation(C)).({o}); {o} c= the carrier of C proof let x be object; assume x in {o}; then x = o by TARSKI:def 1; hence thesis; end; then reconsider t = {o} as Subset of the carrier of C; A c= the carrier' of C proof let x be object; assume x in A; then x in {a where a is Attribute of C : for o being Object of C st o in t holds o is-connected-with a} by Def2; then ex x9 being Attribute of C st x9 = x & for o being Object of C st o in t holds o is-connected-with x9; hence thesis; end; then reconsider A as Subset of the carrier' of C; set O = (AttributeDerivation(C)).((ObjectDerivation(C)).({o})); O c= the carrier of C proof let x be object; assume x in O; then x in {o9 where o9 is Object of C : for a being Attribute of C st a in ((ObjectDerivation(C)).t) holds o9 is-connected-with a} by Def3; then ex x9 being Object of C st x9 = x & for a being Attribute of C st a in ((ObjectDerivation(C)).t) holds x9 is-connected-with a; hence thesis; end; then reconsider O as Subset of the carrier of C; set M9 = ConceptStr(#O,A#); o in {o} & t c= (AttributeDerivation(C)).((ObjectDerivation(C)).t) by Th5, TARSKI:def 1; then reconsider M9 as non empty ConceptStr over C by Def7; (ObjectDerivation(C)).(the Extent of M9) = (ObjectDerivation(C)).t by Th7 .= the Intent of M9; then M9 is concept-like; hence thesis; end; end; definition let C be FormalContext; mode FormalConcept of C is concept-like non empty ConceptStr over C; end; registration let C be FormalContext; cluster strict for FormalConcept of C; existence proof set CP = the FormalConcept of C; A1: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP & ( AttributeDerivation(C)).(the Intent of CP) = the Extent of CP by Def9; the Intent of CP is non empty or the Extent of CP is non empty by Def7; then the ConceptStr of CP is FormalConcept of C by A1,Def7,Def9; hence thesis; end; end; theorem Th19: for C being FormalContext for O being Subset of the carrier of C holds ConceptStr(#(AttributeDerivation(C)).((ObjectDerivation(C)).O), ( ObjectDerivation(C)).O#) is FormalConcept of C & for O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st ConceptStr(#O9,A9#) is FormalConcept of C & O c= O9 holds (AttributeDerivation(C)).((ObjectDerivation( C)).O) c= O9 proof let C be FormalContext; let O be Subset of the carrier of C; A1: for O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st ConceptStr(#O9,A9#) is FormalConcept of C & O c= O9 holds ( AttributeDerivation(C)).((ObjectDerivation(C)).O) c= O9 proof let O9 be Subset of the carrier of C; let A9 be Subset of the carrier' of C; assume that A2: ConceptStr(#O9,A9#) is FormalConcept of C and A3: O c= O9; reconsider M9 = ConceptStr(#O9,A9#) as FormalConcept of C by A2; A4: (AttributeDerivation(C)).(A9) = the Extent of M9 by Def9 .= O9; A5: (ObjectDerivation(C)).(O9) = the Intent of M9 by Def9 .= A9; (ObjectDerivation(C)).(O9) c= (ObjectDerivation(C)).(O) by A3,Th3; hence thesis by A4,A5,Th4; end; ConceptStr(#(AttributeDerivation(C)).((ObjectDerivation(C)).O), ( ObjectDerivation(C)).O#) is FormalConcept of C proof set M9 = ConceptStr(#(AttributeDerivation(C)).((ObjectDerivation(C)).O), ( ObjectDerivation(C)).O#); (ObjectDerivation(C)).(the Extent of M9) = the Intent of M9 by Th7; hence thesis by Def9,Lm1; end; hence thesis by A1; end; theorem for C being FormalContext for O being Subset of the carrier of C holds (ex A being Subset of the carrier' of C st ConceptStr(#O,A#) is FormalConcept of C) iff (AttributeDerivation(C)).((ObjectDerivation(C)).O) = O proof let C be FormalContext; let O be Subset of the carrier of C; A1: now O c= (AttributeDerivation(C)).((ObjectDerivation(C)).O) by Th5; then A2: for x being object holds x in O implies x in (AttributeDerivation(C)).(( ObjectDerivation(C)).O); given A being Subset of the carrier' of C such that A3: ConceptStr(#O,A#) is FormalConcept of C; (AttributeDerivation(C)).((ObjectDerivation(C)).O) c= O by A3,Th19; then for x being object holds x in (AttributeDerivation(C)).((ObjectDerivation (C)).O) implies x in O; hence (AttributeDerivation(C)).((ObjectDerivation(C)).O) = O by A2,TARSKI:2 ; end; now reconsider A = (ObjectDerivation(C)).O as Subset of the carrier' of C; set M9 = ConceptStr(#O,A#); assume (AttributeDerivation(C)).((ObjectDerivation(C)).O) = O; then M9 is FormalConcept of C by Def9,Lm1; hence ex A being Subset of the carrier' of C st ConceptStr(#O,A#) is FormalConcept of C; end; hence thesis by A1; end; theorem Th21: for C being FormalContext for A being Subset of the carrier' of C holds ConceptStr(#(AttributeDerivation(C)).A, (ObjectDerivation(C)).(( AttributeDerivation(C)).A)#) is FormalConcept of C & for O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st ConceptStr(#O9,A9#) is FormalConcept of C & A c= A9 holds (ObjectDerivation(C)).((AttributeDerivation( C)).A) c= A9 proof let C be FormalContext; let A be Subset of the carrier' of C; A1: for O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st ConceptStr(#O9,A9#) is FormalConcept of C & A c= A9 holds ( ObjectDerivation(C)).((AttributeDerivation(C)).A) c= A9 proof let O9 be Subset of the carrier of C; let A9 be Subset of the carrier' of C; assume that A2: ConceptStr(#O9,A9#) is FormalConcept of C and A3: A c= A9; reconsider M9 = ConceptStr(#O9,A9#) as FormalConcept of C by A2; A4: (AttributeDerivation(C)).(A9) = the Extent of M9 by Def9 .= O9; A5: (ObjectDerivation(C)).(O9) = the Intent of M9 by Def9 .= A9; (AttributeDerivation(C)).(A9) c= (AttributeDerivation(C)).(A) by A3,Th4; hence thesis by A4,A5,Th3; end; ConceptStr(#(AttributeDerivation(C)).A, (ObjectDerivation(C)).(( AttributeDerivation(C)).A)#) is FormalConcept of C proof set M9 = ConceptStr(#(AttributeDerivation(C)).A, (ObjectDerivation(C)).(( AttributeDerivation(C)).A)#); (AttributeDerivation(C)).(the Intent of M9) = the Extent of M9 by Th8; hence thesis by Def9,Lm1; end; hence thesis by A1; end; theorem for C being FormalContext for A being Subset of the carrier' of C holds (ex O being Subset of the carrier of C st ConceptStr(#O,A#) is FormalConcept of C) iff (ObjectDerivation(C)).((AttributeDerivation(C)).A) = A proof let C be FormalContext; let A be Subset of the carrier' of C; A1: now A c= (ObjectDerivation(C)).((AttributeDerivation(C)).A) by Th6; then A2: for x being object holds x in A implies x in (ObjectDerivation(C)).(( AttributeDerivation(C)).A); given O being Subset of the carrier of C such that A3: ConceptStr(#O,A#) is FormalConcept of C; (ObjectDerivation(C)).((AttributeDerivation(C)).A) c= A by A3,Th21; then for x being object holds x in (ObjectDerivation(C)).((AttributeDerivation (C)).A) implies x in A; hence (ObjectDerivation(C)).((AttributeDerivation(C)).A) = A by A2,TARSKI:2 ; end; now reconsider O = (AttributeDerivation(C)).A as Subset of the carrier of C; set M9 = ConceptStr(#O,A#); assume (ObjectDerivation(C)).((AttributeDerivation(C)).A) = A; then M9 is FormalConcept of C by Def9,Lm1; hence ex O being Subset of the carrier of C st ConceptStr(#O,A#) is FormalConcept of C; end; hence thesis by A1; end; definition let C be FormalContext; let CP be ConceptStr over C; attr CP is universal means the Extent of CP = the carrier of C; end; definition let C be FormalContext; let CP be ConceptStr over C; attr CP is co-universal means the Intent of CP = the carrier' of C; end; registration let C be FormalContext; cluster strict universal for FormalConcept of C; existence proof reconsider e = {} as Subset of the carrier' of C by XBOOLE_1:2; reconsider CP = ConceptStr(#(AttributeDerivation(C)).(e), ( ObjectDerivation(C)).((AttributeDerivation(C)).(e))#) as FormalConcept of C by Th21; (AttributeDerivation(C)).({}) = the carrier of C by Th18; then CP is universal; hence thesis; end; cluster strict co-universal for FormalConcept of C; existence proof reconsider e = {} as Subset of the carrier of C by XBOOLE_1:2; reconsider CP = ConceptStr(# (AttributeDerivation(C)).((ObjectDerivation(C )).(e)), (ObjectDerivation(C)).(e)#) as FormalConcept of C by Th19; (ObjectDerivation(C)).({}) = the carrier' of C by Th17; then CP is co-universal; hence thesis; end; end; definition let C be FormalContext; func Concept-with-all-Objects(C) -> strict universal FormalConcept of C means :Def12: ex O being Subset of the carrier of C, A being Subset of the carrier' of C st it = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).({}) & A = (ObjectDerivation(C)).((AttributeDerivation(C)).({})); existence proof reconsider e = {} as Subset of the carrier' of C by XBOOLE_1:2; reconsider CP = ConceptStr(#(AttributeDerivation(C)).(e), ( ObjectDerivation(C)).((AttributeDerivation(C)).(e))#) as FormalConcept of C by Th21; (AttributeDerivation(C)).({}) = the carrier of C by Th18; then CP is universal; hence thesis; end; uniqueness; end; definition let C be FormalContext; func Concept-with-all-Attributes(C) -> strict co-universal FormalConcept of C means :Def13: ex O being Subset of the carrier of C, A being Subset of the carrier' of C st it = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).(( ObjectDerivation(C)).({})) & A = (ObjectDerivation(C)).({}); existence proof reconsider e = {} as Subset of the carrier of C by XBOOLE_1:2; reconsider CP = ConceptStr(# (AttributeDerivation(C)).((ObjectDerivation(C )).(e)), (ObjectDerivation(C)).(e)#) as FormalConcept of C by Th19; (ObjectDerivation(C)).({}) = the carrier' of C by Th17; then CP is co-universal; hence thesis; end; uniqueness; end; theorem Th23: for C being FormalContext holds the Extent of Concept-with-all-Objects(C) = the carrier of C & the Intent of Concept-with-all-Attributes(C) = the carrier' of C proof let C be FormalContext; (ex O being Subset of the carrier of C, A being Subset of the carrier' of C st Concept-with-all-Objects(C) = ConceptStr(#O,A#) & O = ( AttributeDerivation(C) ).({}) & A = (ObjectDerivation(C)).((AttributeDerivation (C)).({})) )& ex O being Subset of the carrier of C, A being Subset of the carrier' of C st Concept-with-all-Attributes(C) = ConceptStr(#O,A#) & O = ( AttributeDerivation( C)).((ObjectDerivation(C)).({})) & A = ( ObjectDerivation( C)).({}) by Def12,Def13; hence thesis by Th17,Th18; end; theorem for C being FormalContext for CP being FormalConcept of C holds (the Extent of CP = {} implies CP is co-universal) & (the Intent of CP = {} implies CP is universal) proof let C be FormalContext; let CP be FormalConcept of C; A1: (AttributeDerivation(C)).(the Intent of CP) = the Extent of CP by Def9; A2: the Intent of CP = {} implies CP is universal by A1,Th18; A3: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP by Def9; the Extent of CP = {} implies CP is co-universal by A3,Th17; hence thesis by A2; end; theorem Th25: for C being FormalContext for CP being strict FormalConcept of C holds (the Extent of CP = {} implies CP = Concept-with-all-Attributes(C)) & ( the Intent of CP = {} implies CP = Concept-with-all-Objects(C)) proof let C be FormalContext; let CP be strict FormalConcept of C; A1: (AttributeDerivation(C)).(the Intent of CP) = the Extent of CP by Def9; A2: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP by Def9; A3: now assume A4: the Intent of CP = {}; then the Extent of CP = the carrier of C by A1,Th18; then CP is universal; hence CP = Concept-with-all-Objects(C) by A2,A1,A4,Def12; end; now assume A5: the Extent of CP = {}; then the Intent of CP = the carrier' of C by A2,Th17; then CP is co-universal; hence CP = Concept-with-all-Attributes(C) by A2,A1,A5,Def13; end; hence thesis by A3; end; theorem for C being FormalContext for CP being quasi-empty ConceptStr over C st CP is FormalConcept of C holds CP is universal or CP is co-universal proof let C be FormalContext; let CP be quasi-empty ConceptStr over C; assume CP is FormalConcept of C; then reconsider CP as FormalConcept of C; A1: (AttributeDerivation(C)).(the Intent of CP) = the Extent of CP by Def9; A2: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP by Def9; now per cases by Def8; case the Intent of CP is empty; then the Extent of CP = the carrier of C by A1,Th18; hence CP is universal; end; case the Extent of CP is empty; then the Intent of CP = the carrier' of C by A2,Th17; hence CP is co-universal; end; end; hence thesis; end; theorem for C being FormalContext for CP being quasi-empty ConceptStr over C st CP is strict FormalConcept of C holds CP = Concept-with-all-Objects(C) or CP = Concept-with-all-Attributes(C) proof let C be FormalContext; let CP be quasi-empty ConceptStr over C; assume A1: CP is strict FormalConcept of C; now per cases by Def8; case the Intent of CP is empty; hence CP = Concept-with-all-Objects(C) by A1,Th25; end; case the Extent of CP is empty; hence CP = Concept-with-all-Attributes(C) by A1,Th25; end; end; hence thesis; end; definition let C be FormalContext; mode Set-of-FormalConcepts of C -> non empty set means :Def14: for X being set st X in it holds X is FormalConcept of C; existence proof set CP = the FormalConcept of C; for X being set st X in {CP} holds X is FormalConcept of C by TARSKI:def 1; hence thesis; end; end; definition let C be FormalContext; let FCS be Set-of-FormalConcepts of C; redefine mode Element of FCS -> FormalConcept of C; coherence by Def14; end; definition let C be FormalContext; let CP1,CP2 be FormalConcept of C; pred CP1 is-SubConcept-of CP2 means the Extent of CP1 c= the Extent of CP2; end; notation let C be FormalContext; let CP1,CP2 be FormalConcept of C; synonym CP2 is-SuperConcept-of CP1 for CP1 is-SubConcept-of CP2; end; theorem Th28: for C being FormalContext for CP1,CP2 being FormalConcept of C holds CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 proof let C be FormalContext; let CP1,CP2 be FormalConcept of C; A1: now assume the Intent of CP2 c= the Intent of CP1; then A2: (AttributeDerivation(C)).(the Intent of CP1) c= (AttributeDerivation(C )).(the Intent of CP2) by Th4; (AttributeDerivation(C)).(the Intent of CP1) = the Extent of CP1 & ( AttributeDerivation(C)).(the Intent of CP2) = the Extent of CP2 by Def9; hence CP1 is-SubConcept-of CP2 by A2; end; now assume CP1 is-SubConcept-of CP2; then A3: the Extent of CP1 c= the Extent of CP2; (ObjectDerivation(C)).(the Extent of CP2) = the Intent of CP2 & ( ObjectDerivation(C)).(the Extent of CP1) = the Intent of CP1 by Def9; hence the Intent of CP2 c= the Intent of CP1 by A3,Th3; end; hence thesis by A1; end; theorem for C being FormalContext for CP1,CP2 being FormalConcept of C holds CP1 is-SuperConcept-of CP2 iff the Intent of CP1 c= the Intent of CP2 by Th28; theorem for C being FormalContext for CP being FormalConcept of C holds CP is-SubConcept-of Concept-with-all-Objects(C) & Concept-with-all-Attributes(C) is-SubConcept-of CP proof let C be FormalContext; let CP be FormalConcept of C; A1: the carrier' of C = the Intent of Concept-with-all-Attributes(C) & the Intent of CP c= the carrier' of C by Th23; the carrier of C = the Extent of Concept-with-all-Objects(C) & the Extent of CP c= the carrier of C by Th23; hence thesis by A1,Th28; end; begin :: Concept Lattices definition let C be FormalContext; func B-carrier(C) -> non empty set equals { ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) is non empty & (ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E }; coherence proof set M9 = { ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) is non empty & ( ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E }; M9 is non empty proof set CP = the FormalConcept of C; consider O being Subset of the carrier of C such that A1: O = the Extent of CP; consider A being Subset of the carrier' of C such that A2: A = the Intent of CP; A3: (AttributeDerivation(C)).A = O by A1,A2,Def9; A4: (ObjectDerivation(C)).O = A by A1,A2,Def9; then ConceptStr(#O,A#) is non empty by Lm1; then ConceptStr(#O,A#) in M9 by A4,A3; hence thesis; end; then reconsider M9 as non empty set; for CP being strict non empty ConceptStr over C holds CP in M9 iff ( ObjectDerivation(C)).(the Extent of CP) = the Intent of CP & ( AttributeDerivation(C)).(the Intent of CP) = the Extent of CP proof let CP be strict non empty ConceptStr over C; now assume CP in M9; then ex E being Subset of the carrier of C, I being Subset of the carrier' of C st CP = ConceptStr(#E,I#) & ConceptStr(#E,I#) is non empty & ( ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E; hence (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP & ( AttributeDerivation(C)).(the Intent of CP) = the Extent of CP; end; hence thesis; end; hence thesis; end; end; definition let C be FormalContext; redefine func B-carrier(C) -> Set-of-FormalConcepts of C; coherence proof for X being set holds X in B-carrier(C) implies X is FormalConcept of C proof let X be set; assume X in B-carrier(C); then ex E being Subset of the carrier of C, I being Subset of the carrier' of C st X = ConceptStr(#E,I#) & ConceptStr(#E,I#) is non empty & ( ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E; hence thesis by Def9; end; hence thesis by Def14; end; end; registration let C be FormalContext; cluster B-carrier(C) -> non empty; coherence; end; theorem Th31: for C being FormalContext for CP being object holds CP in B-carrier (C) iff CP is strict FormalConcept of C proof let C be FormalContext; let CP be object; A1: CP is strict FormalConcept of C implies CP in B-carrier(C) proof assume A2: CP is strict FormalConcept of C; then reconsider CP as FormalConcept of C; set I9 = the Intent of CP; set E9 = the Extent of CP; (ObjectDerivation(C)).E9 = I9 & (AttributeDerivation(C)).I9 = E9 by Def9; hence thesis by A2; end; CP in B-carrier(C) implies CP is strict FormalConcept of C proof assume CP in B-carrier(C); then ex E being Subset of the carrier of C, I being Subset of the carrier' of C st CP = ConceptStr(#E,I#) & ConceptStr(#E,I#) is non empty & ( ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E; hence thesis by Def9; end; hence thesis by A1; end; definition let C be FormalContext; func B-meet(C) -> BinOp of B-carrier(C) means :Def17: for CP1,CP2 being strict FormalConcept of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st it.(CP1,CP2) = ConceptStr(#O,A#) & O = (the Extent of CP1) /\ (the Extent of CP2) & A = (ObjectDerivation(C)).(( AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2))); existence proof defpred P[FormalConcept of C, FormalConcept of C, set] means ex O being Subset of the carrier of C, A being Subset of the carrier' of C st ($3 = ConceptStr(#O,A#) & O = (the Extent of $1) /\ (the Extent of $2) & A = ( ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of $1) \/ (the Intent of $2)))); A1: for CP1 being Element of B-carrier(C), CP2 being Element of B-carrier( C) ex CP being Element of B-carrier(C) st P[CP1,CP2,CP] proof let CP1 be Element of B-carrier(C); let CP2 be Element of B-carrier(C); set O = (the Extent of CP1) /\ (the Extent of CP2); set A = (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2))); reconsider A9 = (the Intent of CP1) \/ (the Intent of CP2) as Subset of the carrier' of C; set CP = ConceptStr(#O,A#); A2: (AttributeDerivation(C)).A = (AttributeDerivation(C)).A9 by Th8 .= (AttributeDerivation(C)).(the Intent of CP1) /\ ( AttributeDerivation(C)).(the Intent of CP2) by Th16 .= (the Extent of CP1) /\ (AttributeDerivation(C)).(the Intent of CP2) by Def9 .= (the Extent of CP1) /\ (the Extent of CP2) by Def9; then A3: (ObjectDerivation(C)).O = A by Th7; then ConceptStr(#O,A#) is non empty by Lm1; then CP in {ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) is non empty & ( ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E } by A2,A3; hence thesis; end; consider f being Function of [:B-carrier(C),B-carrier(C):],B-carrier(C) such that A4: for CP1 being Element of B-carrier(C), CP2 being Element of B-carrier(C) holds P[CP1,CP2,f.(CP1,CP2)] from BINOP_1:sch 3(A1); reconsider f as BinOp of B-carrier(C); take f; for CP1,CP2 being strict FormalConcept of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st f.(CP1,CP2) = ConceptStr(#O,A#) & O = (the Extent of CP1) /\ (the Extent of CP2) & A = ( ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2))) proof let CP1,CP2 be strict FormalConcept of C; CP1 is Element of B-carrier(C) & CP2 is Element of B-carrier(C) by Th31; hence thesis by A4; end; hence thesis; end; uniqueness proof let F1,F2 be BinOp of B-carrier(C); assume A5: for CP1,CP2 being strict FormalConcept of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st F1.(CP1,CP2) = ConceptStr(#O,A#) & O = (the Extent of CP1) /\ (the Extent of CP2) & A = ( ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2))); assume A6: for CP1,CP2 being strict FormalConcept of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st F2.(CP1,CP2) = ConceptStr(#O,A#) & O = (the Extent of CP1) /\ (the Extent of CP2) & A = ( ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2))); A7: for X being object st X in [:B-carrier(C),B-carrier(C):] holds F1.X = F2 .X proof let X be object; assume X in [:B-carrier(C),B-carrier(C):]; then consider A,B being object such that A8: A in B-carrier(C) and A9: B in B-carrier(C) and A10: X = [A,B] by ZFMISC_1:def 2; reconsider B as strict FormalConcept of C by A9,Th31; reconsider A as strict FormalConcept of C by A8,Th31; (ex O being Subset of the carrier of C, At being Subset of the carrier' of C st F1.(A,B) = ConceptStr(#O,At#) & O = (the Extent of A) /\ (the Extent of B) & At = (ObjectDerivation(C)).((AttributeDerivation(C)). ( (the Intent of A) \/ ( the Intent of B))) )& ex O9 being Subset of the carrier of C, At9 being Subset of the carrier' of C st F2.(A,B) = ConceptStr(#O9,At9#) & O9 = (the Extent of A ) /\ (the Extent of B) & At9 = (ObjectDerivation(C)).(( AttributeDerivation(C)) . ((the Intent of A) \/ (the Intent of B))) by A5,A6; hence thesis by A10; end; dom F1 = [:B-carrier(C),B-carrier(C):] & dom F2 = [:B-carrier(C), B-carrier(C ):] by FUNCT_2:def 1; hence thesis by A7,FUNCT_1:2; end; end; definition let C be FormalContext; func B-join(C) -> BinOp of B-carrier(C) means :Def18: for CP1,CP2 being strict FormalConcept of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st it.(CP1,CP2) = ConceptStr(#O,A#) & O = ( AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2))) & A = (the Intent of CP1) /\ (the Intent of CP2); existence proof defpred P[FormalConcept of C, FormalConcept of C, set] means ex O being Subset of the carrier of C, A being Subset of the carrier' of C st ($3 = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of $1) \/ (the Extent of $2))) & A = (the Intent of $1) /\ (the Intent of $2)); A1: for CP1 being Element of B-carrier(C), CP2 being Element of B-carrier( C) ex CP being Element of B-carrier(C) st P[CP1,CP2,CP] proof let CP1 be Element of B-carrier(C); let CP2 be Element of B-carrier(C); set O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2))); set A = (the Intent of CP1) /\ (the Intent of CP2); reconsider O9 = (the Extent of CP1) \/ (the Extent of CP2) as Subset of the carrier of C; set CP = ConceptStr(#O,A#); A2: (ObjectDerivation(C)).O = (ObjectDerivation(C)).O9 by Th7 .= (ObjectDerivation(C)).(the Extent of CP1) /\ (ObjectDerivation(C) ).(the Extent of CP2) by Th15 .= (the Intent of CP1) /\ (ObjectDerivation(C)).(the Extent of CP2) by Def9 .= (the Intent of CP1) /\ (the Intent of CP2) by Def9; then (AttributeDerivation(C)).A = O & ConceptStr(#O,A#) is non empty by Lm1,Th7; then CP in {ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) is non empty & ( ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E } by A2; hence thesis; end; consider f being Function of [:B-carrier(C),B-carrier(C):],B-carrier(C) such that A3: for CP1 being Element of B-carrier(C), CP2 being Element of B-carrier(C) holds P[CP1,CP2,f.(CP1,CP2)] from BINOP_1:sch 3(A1); reconsider f as BinOp of B-carrier(C); take f; for CP1,CP2 being strict FormalConcept of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st f.(CP1,CP2) = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2))) & A = (the Intent of CP1) /\ (the Intent of CP2) proof let CP1,CP2 be strict FormalConcept of C; CP1 is Element of B-carrier(C) & CP2 is Element of B-carrier(C) by Th31; hence thesis by A3; end; hence thesis; end; uniqueness proof let F1,F2 be BinOp of B-carrier(C); assume A4: for CP1,CP2 being strict FormalConcept of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st F1.(CP1,CP2) = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((ObjectDerivation(C)). (( the Extent of CP1) \/ (the Extent of CP2))) & A = (the Intent of CP1) /\ (the Intent of CP2); assume A5: for CP1,CP2 being strict FormalConcept of C holds ex O being Subset of the carrier of C, A being Subset of the carrier' of C st F2.(CP1,CP2) = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((ObjectDerivation(C)). (( the Extent of CP1) \/ (the Extent of CP2))) & A = (the Intent of CP1) /\ (the Intent of CP2); A6: for X being object st X in [:B-carrier(C),B-carrier(C):] holds F1.X = F2 .X proof let X be object; assume X in [:B-carrier(C),B-carrier(C):]; then consider A,B being object such that A7: A in B-carrier(C) and A8: B in B-carrier(C) and A9: X = [A,B] by ZFMISC_1:def 2; reconsider B as strict FormalConcept of C by A8,Th31; reconsider A as strict FormalConcept of C by A7,Th31; (ex O being Subset of the carrier of C, At being Subset of the carrier' of C st F1.(A,B) = ConceptStr(#O,At#) & O = ( AttributeDerivation(C)). (( ObjectDerivation(C)). ((the Extent of A) \/ (the Extent of B))) & At = (the Intent of A) /\ (the Intent of B) )& ex O9 being Subset of the carrier of C, At9 being Subset of the carrier' of C st F2.(A,B) = ConceptStr(#O9,At9#) & O9 = ( AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of A) \/ ( the Extent of B))) & At9 = (the Intent of A) /\ (the Intent of B) by A4,A5; hence thesis by A9; end; dom F1 = [:B-carrier(C),B-carrier(C):] & dom F2 = [:B-carrier(C), B-carrier(C ):] by FUNCT_2:def 1; hence thesis by A6,FUNCT_1:2; end; end; Lm2: for C being FormalContext for CP1,CP2 being strict FormalConcept of C holds (B-meet(C)).(CP1,CP2) in rng((B-meet(C))) proof let C be FormalContext; let CP1,CP2 be strict FormalConcept of C; CP1 in B-carrier(C) & CP2 in B-carrier(C) by Th31; then [CP1,CP2] in [:B-carrier(C),B-carrier(C):] by ZFMISC_1:def 2; then [CP1,CP2] in dom((B-meet(C))) by FUNCT_2:def 1; hence thesis by FUNCT_1:def 3; end; Lm3: for C being FormalContext for CP1,CP2 being strict FormalConcept of C holds (B-join(C)).(CP1,CP2) in rng((B-join(C))) proof let C be FormalContext; let CP1,CP2 be strict FormalConcept of C; CP1 in B-carrier(C) & CP2 in B-carrier(C) by Th31; then [CP1,CP2] in [:B-carrier(C),B-carrier(C):] by ZFMISC_1:def 2; then [CP1,CP2] in dom((B-join(C))) by FUNCT_2:def 1; hence thesis by FUNCT_1:def 3; end; theorem Th32: for C being FormalContext for CP1,CP2 being strict FormalConcept of C holds (B-meet(C)).(CP1,CP2) = (B-meet(C)).(CP2,CP1) proof let C be FormalContext; let CP1,CP2 be strict FormalConcept of C; (ex O being Subset of the carrier of C, A being Subset of the carrier' of C st (B-meet(C)).(CP1,CP2) = ConceptStr(#O,A#) & O = (the Extent of CP1) /\ (the Extent of CP2) & A = (ObjectDerivation(C)).(( AttributeDerivation(C)). (( the Intent of CP1) \/ (the Intent of CP2))) )& ex O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st (B-meet(C)).(CP2,CP1) = ConceptStr (#O9,A9#) & O9 = (the Extent of CP2) /\ (the Extent of CP1) & A9 = ( ObjectDerivation(C)).(( AttributeDerivation(C)). ((the Intent of CP2) \/ (the Intent of CP1))) by Def17; hence thesis; end; theorem Th33: for C being FormalContext for CP1,CP2 being strict FormalConcept of C holds (B-join(C)).(CP1,CP2) = (B-join(C)).(CP2,CP1) proof let C be FormalContext; let CP1,CP2 be strict FormalConcept of C; (ex O being Subset of the carrier of C, A being Subset of the carrier' of C st (B-join(C)).(CP1,CP2) = ConceptStr(#O,A#) & O = ( AttributeDerivation(C )).(( ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2))) & A = (the Intent of CP1) /\ (the Intent of CP2) )& ex O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st (B-join(C)).(CP2,CP1) = ConceptStr (#O9,A9#) & O9 = ( AttributeDerivation(C)).((ObjectDerivation(C)). ( (the Extent of CP2) \/ (the Extent of CP1))) & A9 = (the Intent of CP2) /\ (the Intent of CP1) by Def18; hence thesis; end; theorem Th34: for C being FormalContext for CP1,CP2,CP3 being strict FormalConcept of C holds (B-meet(C)).(CP1,(B-meet(C)).(CP2,CP3)) = (B-meet(C)). ((B-meet(C)).(CP1,CP2),CP3) proof let C be FormalContext; let CP1,CP2,CP3 be strict FormalConcept of C; (B-meet(C)).(CP1,CP2) in rng((B-meet(C))) by Lm2; then reconsider CP = (B-meet(C)).(CP1,CP2) as strict FormalConcept of C by Th31; A1: (ex O being Subset of the carrier of C, A being Subset of the carrier' of C st (B-meet(C)).(CP1,CP2) = ConceptStr(#O,A#) & O = (the Extent of CP1) /\ (the Extent of CP2) & A = (ObjectDerivation(C)).(( AttributeDerivation(C)). (( the Intent of CP1) \/ (the Intent of CP2))) )& ex O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st (B-meet(C)).(CP,CP3) = ConceptStr (#O9,A9#) & O9 = (the Extent of CP) /\ (the Extent of CP3) & A9 = ( ObjectDerivation(C)).(( AttributeDerivation(C)). ((the Intent of CP) \/ (the Intent of CP3))) by Def17; (B-meet(C)).(CP2,CP3) in rng((B-meet(C))) by Lm2; then reconsider CP9 = (B-meet(C)).(CP2,CP3) as strict FormalConcept of C by Th31; A2: (ex O being Subset of the carrier of C, A being Subset of the carrier' of C st (B-meet(C)).(CP2,CP3) = ConceptStr(#O,A#) & O = (the Extent of CP2) /\ (the Extent of CP3) & A = (ObjectDerivation(C)).(( AttributeDerivation(C)). (( the Intent of CP2) \/ (the Intent of CP3))) )& ex O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st (B-meet(C)).(CP1,CP9) = ConceptStr (#O9,A9#) & O9 = (the Extent of CP1) /\ (the Extent of CP9) & A9 = ( ObjectDerivation(C)).(( AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP9))) by Def17; (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ ((ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP2) \/ (the Intent of CP3)))))) = (ObjectDerivation(C)). (((AttributeDerivation(C)).(the Intent of CP1)) /\ ((AttributeDerivation(C)). ((ObjectDerivation(C)).(( AttributeDerivation(C)). ((the Intent of CP2) \/ (the Intent of CP3)))))) by Th16 .= (ObjectDerivation(C)). (((AttributeDerivation(C)).(the Intent of CP1) ) /\ ((AttributeDerivation(C)). ((the Intent of CP2) \/ (the Intent of CP3)))) by Th8 .= (ObjectDerivation(C)). (((AttributeDerivation(C)).(the Intent of CP1) ) /\ (((AttributeDerivation(C)).(the Intent of CP2)) /\ ((AttributeDerivation(C )).(the Intent of CP3)))) by Th16 .= (ObjectDerivation(C)). ((((AttributeDerivation(C)).(the Intent of CP1 )) /\ ((AttributeDerivation(C)).(the Intent of CP2))) /\ ((AttributeDerivation( C)).(the Intent of CP3))) by XBOOLE_1:16 .= (ObjectDerivation(C)). (((AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2)) /\ ((AttributeDerivation(C)).(the Intent of CP3))) ) by Th16 .= (ObjectDerivation(C)). (((AttributeDerivation(C)). ((ObjectDerivation (C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2)))) /\ ((AttributeDerivation(C)).(the Intent of CP3)))) by Th8 .= (ObjectDerivation(C)).((AttributeDerivation(C)). (((ObjectDerivation( C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2)))) \/ (the Intent of CP3))) by Th16; hence thesis by A1,A2,XBOOLE_1:16; end; theorem Th35: for C being FormalContext for CP1,CP2,CP3 being strict FormalConcept of C holds (B-join(C)).(CP1,(B-join(C)).(CP2,CP3)) = (B-join(C)). ((B-join(C)).(CP1,CP2),CP3) proof let C be FormalContext; let CP1,CP2,CP3 be strict FormalConcept of C; (B-join(C)).(CP1,CP2) in rng((B-join(C))) by Lm3; then reconsider CP = (B-join(C)).(CP1,CP2) as strict FormalConcept of C by Th31; A1: (ex O being Subset of the carrier of C, A being Subset of the carrier' of C st (B-join(C)).(CP1,CP2) = ConceptStr(#O,A#) & O = ( AttributeDerivation(C )).(( ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2))) & A = (the Intent of CP1) /\ (the Intent of CP2) )& ex O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st (B-join(C)).(CP,CP3) = ConceptStr(# O9,A9#) & O9 = ( AttributeDerivation(C)).((ObjectDerivation(C)). ( (the Extent of CP) \/ (the Extent of CP3))) & A9 = (the Intent of CP) /\ (the Intent of CP3) by Def18; (B-join(C)).(CP2,CP3) in rng((B-join(C))) by Lm3; then reconsider CP9 = (B-join(C)).(CP2,CP3) as strict FormalConcept of C by Th31; A2: (ex O being Subset of the carrier of C, A being Subset of the carrier' of C st (B-join(C)).(CP2,CP3) = ConceptStr(#O,A#) & O = ( AttributeDerivation(C )).(( ObjectDerivation(C)). ((the Extent of CP2) \/ (the Extent of CP3))) & A = (the Intent of CP2) /\ (the Intent of CP3) )& ex O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st (B-join(C)).(CP1,CP9) = ConceptStr (#O9,A9#) & O9 = ( AttributeDerivation(C)).((ObjectDerivation(C)). ( (the Extent of CP1) \/ (the Extent of CP9))) & A9 = (the Intent of CP1) /\ (the Intent of CP9) by Def18; (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1) \/ ((AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP2) \/ (the Extent of CP3)))))) = (AttributeDerivation(C)). (((ObjectDerivation(C)).(the Extent of CP1)) /\ ((ObjectDerivation(C)). ((AttributeDerivation(C)).(( ObjectDerivation(C)). ((the Extent of CP2) \/ (the Extent of CP3)))))) by Th15 .= (AttributeDerivation(C)). (((ObjectDerivation(C)).(the Extent of CP1) ) /\ ((ObjectDerivation(C)). ((the Extent of CP2) \/ (the Extent of CP3)))) by Th7 .= (AttributeDerivation(C)). (((ObjectDerivation(C)).(the Extent of CP1) ) /\ (((ObjectDerivation(C)).(the Extent of CP2)) /\ ((ObjectDerivation(C)).( the Extent of CP3)))) by Th15 .= (AttributeDerivation(C)). ((((ObjectDerivation(C)).(the Extent of CP1 )) /\ ((ObjectDerivation(C)).(the Extent of CP2))) /\ ((ObjectDerivation(C)).( the Extent of CP3))) by XBOOLE_1:16 .= (AttributeDerivation(C)). (((ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2)) /\ ((ObjectDerivation(C)).(the Extent of CP3)))) by Th15 .= (AttributeDerivation(C)). (((ObjectDerivation(C)). (( AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2)))) /\ ((ObjectDerivation(C)).(the Extent of CP3)))) by Th7 .= (AttributeDerivation(C)).((ObjectDerivation(C)). ((( AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2)))) \/ (the Extent of CP3))) by Th15; hence thesis by A1,A2,XBOOLE_1:16; end; theorem Th36: for C being FormalContext for CP1,CP2 being strict FormalConcept of C holds (B-join(C)).((B-meet(C)).(CP1,CP2),CP2) = CP2 proof let C be FormalContext; let CP1,CP2 be strict FormalConcept of C; A1: ((the Extent of CP1) /\ (the Extent of CP2)) c= (the Extent of CP2) by XBOOLE_1:17; (B-meet(C)).(CP1,CP2) in rng((B-meet(C))) by Lm2; then reconsider CP9 = (B-meet(C)).(CP1,CP2) as strict FormalConcept of C by Th31; A2: (ex O being Subset of the carrier of C, A being Subset of the carrier' of C st (B-meet(C)).(CP1,CP2) = ConceptStr(#O,A#) & O = (the Extent of CP1) /\ (the Extent of CP2) & A = (ObjectDerivation(C)).(( AttributeDerivation(C)). (( the Intent of CP1) \/ (the Intent of CP2))) )& ex O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st (B-join(C)).(CP9,CP2) = ConceptStr (#O9,A9#) & O9 = ( AttributeDerivation(C)).((ObjectDerivation(C)). ( (the Extent of CP9) \/ (the Extent of CP2))) & A9 = (the Intent of CP9) /\ (the Intent of CP2) by Def17,Def18; (AttributeDerivation(C)).((ObjectDerivation(C)). (((the Extent of CP1) /\ (the Extent of CP2)) \/ (the Extent of CP2))) = (AttributeDerivation(C)). (( (ObjectDerivation(C)).((the Extent of CP1) /\ (the Extent of CP2))) /\ (( ObjectDerivation(C)).(the Extent of CP2))) by Th15; then A3: (AttributeDerivation(C)).((ObjectDerivation(C)). (((the Extent of CP1) /\ (the Extent of CP2)) \/ (the Extent of CP2))) = (AttributeDerivation(C)).(( ObjectDerivation(C)).(the Extent of CP2)) by A1,Th3,XBOOLE_1:28 .= (AttributeDerivation(C)).(the Intent of CP2) by Def9 .= the Extent of CP2 by Def9; ((ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2)))) /\ (the Intent of CP2) = ((ObjectDerivation(C)). ((( AttributeDerivation(C)).(the Intent of CP1)) /\ ((AttributeDerivation(C)).(the Intent of CP2)))) /\ (the Intent of CP2) by Th16 .= ((ObjectDerivation(C)). ((the Extent of CP1) /\ ((AttributeDerivation (C)).(the Intent of CP2)))) /\ (the Intent of CP2) by Def9 .= ((ObjectDerivation(C)). ((the Extent of CP1) /\ (the Extent of CP2))) /\ (the Intent of CP2) by Def9 .= ((ObjectDerivation(C)). ((the Extent of CP1) /\ (the Extent of CP2))) /\ ((ObjectDerivation(C)).(the Extent of CP2)) by Def9 .= (ObjectDerivation(C)).(the Extent of CP2) by A1,Th3,XBOOLE_1:28 .= the Intent of CP2 by Def9; hence thesis by A2,A3; end; theorem Th37: for C being FormalContext for CP1,CP2 being strict FormalConcept of C holds (B-meet(C)).(CP1,(B-join(C)).(CP1,CP2)) = CP1 proof let C be FormalContext; let CP1,CP2 be strict FormalConcept of C; A1: ((the Intent of CP1) /\ (the Intent of CP2)) c= (the Intent of CP1) by XBOOLE_1:17; (B-join(C)).(CP1,CP2) in rng((B-join(C))) by Lm3; then reconsider CP9 = (B-join(C)).(CP1,CP2) as strict FormalConcept of C by Th31; A2: (ex O being Subset of the carrier of C, A being Subset of the carrier' of C st (B-join(C)).(CP1,CP2) = ConceptStr(#O,A#) & O = ( AttributeDerivation(C )).(( ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2))) & A = (the Intent of CP1) /\ (the Intent of CP2) )& ex O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C st (B-meet(C)).(CP1,CP9) = ConceptStr (#O9,A9#) & O9 = (the Extent of CP1) /\ (the Extent of CP9) & A9 = ( ObjectDerivation(C)).(( AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP9))) by Def17,Def18; (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ ((the Intent of CP1) /\ (the Intent of CP2)))) = (ObjectDerivation(C)). ((( AttributeDerivation(C)).(the Intent of CP1)) /\ ((AttributeDerivation(C)).((the Intent of CP1) /\ (the Intent of CP2)))) by Th16; then A3: (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ ((the Intent of CP1) /\ (the Intent of CP2)))) = (ObjectDerivation(C)).(( AttributeDerivation(C)).(the Intent of CP1)) by A1,Th4,XBOOLE_1:28 .= (ObjectDerivation(C)).(the Extent of CP1) by Def9 .= the Intent of CP1 by Def9; (the Extent of CP1) /\ ((AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2)))) = (the Extent of CP1) /\ (( AttributeDerivation(C)). (((ObjectDerivation(C)).(the Extent of CP1)) /\ (( ObjectDerivation(C)).(the Extent of CP2)))) by Th15 .= (the Extent of CP1) /\ ((AttributeDerivation(C)). ((the Intent of CP1 ) /\ ((ObjectDerivation(C)).(the Extent of CP2)))) by Def9 .= (the Extent of CP1) /\ ((AttributeDerivation(C)). ((the Intent of CP1 ) /\ (the Intent of CP2))) by Def9 .= ((AttributeDerivation(C)).(the Intent of CP1)) /\ (( AttributeDerivation(C)). ((the Intent of CP1) /\ (the Intent of CP2))) by Def9 .= (AttributeDerivation(C)).(the Intent of CP1) by A1,Th4,XBOOLE_1:28 .= the Extent of CP1 by Def9; hence thesis by A2,A3; end; theorem for C being FormalContext for CP being strict FormalConcept of C holds (B-meet(C)).(CP,Concept-with-all-Objects(C)) = CP proof let C be FormalContext; let CP be strict FormalConcept of C; consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A1: (B-meet(C)).(CP,Concept-with-all-Objects(C)) = ConceptStr(#O,A#) and A2: O = (the Extent of CP) /\ (the Extent of Concept-with-all-Objects(C) ) and A3: A = (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP) \/ (the Intent of Concept-with-all-Objects(C)))) by Def17; A4: O = (the Extent of CP) /\ the carrier of C by A2,Th23 .= the Extent of CP by XBOOLE_1:28; the carrier of C c= the carrier of C; then reconsider O9 = the carrier of C as Subset of the carrier of C; A5: (ObjectDerivation(C)).(the Extent of CP) \/ (ObjectDerivation(C)).O9 = ( ObjectDerivation(C)).(the Extent of CP) by Th3,XBOOLE_1:12; A = (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP) \/ (ObjectDerivation(C)).(the Extent of Concept-with-all-Objects(C)))) by A3 ,Def9 .= (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP) \/ (ObjectDerivation(C)). the carrier of C)) by Th23 .= (ObjectDerivation(C)).((AttributeDerivation(C)). ((ObjectDerivation(C )).(the Extent of CP))) by A5,Def9 .= (ObjectDerivation(C)).(the Extent of CP) by Th7 .= the Intent of CP by Def9; hence thesis by A1,A4; end; theorem Th39: for C being FormalContext for CP being strict FormalConcept of C holds (B-join(C)).(CP,Concept-with-all-Objects(C)) = Concept-with-all-Objects(C ) proof let C be FormalContext; let CP be strict FormalConcept of C; consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A1: (B-join(C)).(CP,Concept-with-all-Objects(C)) = ConceptStr(#O,A#) and A2: O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP) \/ (the Extent of Concept-with-all-Objects(C)))) and A3: A = (the Intent of CP) /\ (the Intent of Concept-with-all-Objects(C) ) by Def18; A4: O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP) \/ the carrier of C)) by A2,Th23 .= (AttributeDerivation(C)).((ObjectDerivation(C)). the carrier of C) by XBOOLE_1:12 .= (AttributeDerivation(C)).((ObjectDerivation(C)). (the Extent of Concept-with-all-Objects(C))) by Th23 .= (AttributeDerivation(C)). (the Intent of Concept-with-all-Objects(C)) by Def9 .= the Extent of Concept-with-all-Objects(C) by Def9; A = ((ObjectDerivation(C)).(the Extent of CP)) /\ (the Intent of Concept-with-all-Objects(C)) by A3,Def9 .= ((ObjectDerivation(C)).(the Extent of CP)) /\ ((ObjectDerivation(C)). (the Extent of Concept-with-all-Objects(C))) by Def9 .= (ObjectDerivation(C)). ((the Extent of CP) \/ (the Extent of Concept-with-all-Objects(C))) by Th15 .= (ObjectDerivation(C)). ((the Extent of CP) \/ the carrier of C) by Th23 .= (ObjectDerivation(C)). the carrier of C by XBOOLE_1:12 .= (ObjectDerivation(C)).(the Extent of Concept-with-all-Objects(C)) by Th23 .= the Intent of Concept-with-all-Objects(C) by Def9; hence thesis by A1,A4; end; theorem for C being FormalContext for CP being strict FormalConcept of C holds (B-join(C)).(CP,Concept-with-all-Attributes(C)) = CP proof let C be FormalContext; let CP be strict FormalConcept of C; consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A1: (B-join(C)).(CP,Concept-with-all-Attributes(C)) = ConceptStr(#O,A#) and A2: O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP) \/ (the Extent of Concept-with-all-Attributes(C)))) and A3: A = (the Intent of CP) /\ (the Intent of Concept-with-all-Attributes (C)) by Def18; A4: A = (the Intent of CP) /\ the carrier' of C by A3,Th23 .= the Intent of CP by XBOOLE_1:28; the carrier' of C c= the carrier' of C; then reconsider A9 = the carrier' of C as Subset of the carrier' of C; A5: (AttributeDerivation(C)).(the Intent of CP) \/ (AttributeDerivation(C) ) .A9 = (AttributeDerivation(C)).(the Intent of CP) by Th4,XBOOLE_1:12; O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP) \/ (AttributeDerivation(C)).(the Intent of Concept-with-all-Attributes(C)))) by A2,Def9 .= (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP) \/ (AttributeDerivation(C)). the carrier' of C)) by Th23 .= (AttributeDerivation(C)).((ObjectDerivation(C)). (( AttributeDerivation(C)).(the Intent of CP))) by A5,Def9 .= (AttributeDerivation(C)).(the Intent of CP) by Th8 .= the Extent of CP by Def9; hence thesis by A1,A4; end; theorem for C being FormalContext for CP being strict FormalConcept of C holds (B-meet(C)).(CP,Concept-with-all-Attributes(C)) = Concept-with-all-Attributes(C ) proof let C be FormalContext; let CP be strict FormalConcept of C; consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A1: (B-meet(C)).(CP,Concept-with-all-Attributes(C)) = ConceptStr(#O,A#) and A2: O = (the Extent of CP) /\ (the Extent of Concept-with-all-Attributes (C)) and A3: A = (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP) \/ (the Intent of Concept-with-all-Attributes(C)))) by Def17; A4: A = (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP) \/ the carrier' of C)) by A3,Th23 .= (ObjectDerivation(C)).((AttributeDerivation(C)). the carrier' of C) by XBOOLE_1:12 .= (ObjectDerivation(C)).((AttributeDerivation(C)). (the Intent of Concept-with-all-Attributes(C))) by Th23 .= (ObjectDerivation(C)).(the Extent of Concept-with-all-Attributes(C)) by Def9 .= the Intent of Concept-with-all-Attributes(C) by Def9; O = ((AttributeDerivation(C)).(the Intent of CP)) /\ (the Extent of Concept-with-all-Attributes(C)) by A2,Def9 .= ((AttributeDerivation(C)).(the Intent of CP)) /\ (( AttributeDerivation(C)). (the Intent of Concept-with-all-Attributes(C))) by Def9 .= (AttributeDerivation(C)). ((the Intent of CP) \/ (the Intent of Concept-with-all-Attributes(C))) by Th16 .= (AttributeDerivation(C)). ((the Intent of CP) \/ the carrier' of C) by Th23 .= (AttributeDerivation(C)). the carrier' of C by XBOOLE_1:12 .= (AttributeDerivation(C)).(the Intent of Concept-with-all-Attributes(C )) by Th23 .= the Extent of Concept-with-all-Attributes(C) by Def9; hence thesis by A1,A4; end; definition let C be FormalContext; func ConceptLattice(C) -> strict non empty LattStr equals LattStr(#B-carrier (C),B-join(C),B-meet(C)#); coherence; end; theorem Th42: for C being FormalContext holds ConceptLattice(C) is Lattice proof let C be FormalContext; set L = LattStr(#B-carrier(C),B-join(C),B-meet(C)#); reconsider L as strict non empty LattStr; A1: for a,b,c being Element of L holds a"\/"(b"\/"c) = (a"\/"b) "\/"c proof let a,b,c be Element of L; reconsider b,c as Element of B-carrier(C); reconsider d = (B-join(C)).(b,c) as Element of L; reconsider b,c as Element of L; reconsider a,b as Element of B-carrier(C); reconsider e = (B-join(C)).(a,b) as Element of L; reconsider a,b as Element of L; A2: a"\/"(b"\/"c) = a"\/"d by LATTICES:def 1 .= (B-join(C)).(a,(B-join(C)).(b,c)) by LATTICES:def 1; A3: (a"\/"b)"\/"c = e"\/"c by LATTICES:def 1 .= (B-join(C)).((B-join(C)).(a,b),c) by LATTICES:def 1; reconsider a,b,c as strict FormalConcept of C by Th31; (B-join(C)).(a,(B-join(C)).(b,c)) = (B-join(C)).((B-join(C)).(a,b),c) by Th35; hence thesis by A2,A3; end; A4: for a,b being Element of L holds (a"/\"b)"\/"b = b proof let a,b be Element of L; reconsider a,b as Element of B-carrier(C); reconsider d = (B-meet(C)).(a,b) as Element of L; reconsider a,b as Element of L; A5: (a"/\"b)"\/"b = d"\/"b by LATTICES:def 2 .= (B-join(C)).((B-meet(C)).(a,b),b) by LATTICES:def 1; reconsider a,b as strict FormalConcept of C by Th31; (B-join(C)).((B-meet(C)).(a,b),b) = b by Th36; hence thesis by A5; end; A6: for a,b,c being Element of L holds a"/\"(b"/\"c) = (a"/\" b)"/\"c proof let a,b,c be Element of L; reconsider b,c as Element of B-carrier(C); reconsider d = (B-meet(C)).(b,c) as Element of L; reconsider b,c as Element of L; A7: a"/\"(b"/\"c) = a"/\"d by LATTICES:def 2 .= (B-meet(C)).(a,(B-meet(C)).(b,c)) by LATTICES:def 2; reconsider a,b as Element of B-carrier(C); reconsider e = (B-meet(C)).(a,b) as Element of L; reconsider a,b as Element of L; A8: (a"/\"b)"/\"c = e"/\"c by LATTICES:def 2 .= (B-meet(C)).((B-meet(C)).(a,b),c) by LATTICES:def 2; reconsider a,b,c as strict FormalConcept of C by Th31; (B-meet(C)).(a,(B-meet(C)).(b,c)) = (B-meet(C)).((B-meet(C)).(a,b),c) by Th34; hence thesis by A7,A8; end; A9: for a,b being Element of L holds a"/\"b = b"/\"a proof let a,b be Element of L; A10: b"/\"a = (B-meet(C)).(b,a) by LATTICES:def 2; reconsider a,b as strict FormalConcept of C by Th31; (B-meet(C)).(a,b) = (B-meet(C)).(b,a) by Th32; hence thesis by A10,LATTICES:def 2; end; A11: for a,b being Element of L holds a"/\"(a"\/"b)=a proof let a,b be Element of L; reconsider a,b as Element of B-carrier(C); reconsider d = (B-join(C)).(a,b) as Element of L; reconsider a,b as Element of L; A12: a"/\"(a"\/"b) = a"/\"d by LATTICES:def 1 .= (B-meet(C)).(a,(B-join(C)).(a,b)) by LATTICES:def 2; reconsider a,b as strict FormalConcept of C by Th31; (B-meet(C)).(a,(B-join(C)).(a,b)) = a by Th37; hence thesis by A12; end; for a,b being Element of L holds a"\/"b = b"\/"a proof let a,b be Element of L; A13: b"\/"a = (B-join(C)).(b,a) by LATTICES:def 1; reconsider a,b as strict FormalConcept of C by Th31; (B-join(C)).(a,b) = (B-join(C)).(b,a) by Th33; hence thesis by A13,LATTICES:def 1; end; then L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A1,A4,A9,A6,A11,LATTICES:def 4,def 5,def 6 ,def 7,def 8,def 9; hence thesis; end; registration let C be FormalContext; cluster ConceptLattice(C) -> strict non empty Lattice-like; coherence by Th42; end; definition let C be FormalContext; let S be non empty Subset of ConceptLattice(C); redefine mode Element of S -> FormalConcept of C; coherence proof let s be Element of S; s is Element of B-carrier(C); hence thesis; end; end; definition let C be FormalContext; let CP be Element of ConceptLattice(C); func CP@ -> strict FormalConcept of C equals CP; coherence by Th31; end; theorem Th43: for C being FormalContext for CP1,CP2 being Element of ConceptLattice(C) holds CP1 [= CP2 iff CP1@ is-SubConcept-of CP2@ proof let C be FormalContext; let CP1,CP2 be Element of ConceptLattice(C); set CL = ConceptLattice(C); A1: now assume A2: CP1@ is-SubConcept-of CP2@; then the Intent of CP2@ c= the Intent of CP1@ by Th28; then A3: (the Intent of CP1@) /\ (the Intent of CP2@) = the Intent of CP2@ by XBOOLE_1:28; consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that A4: (B-join(C)).(CP1@,CP2@) = ConceptStr(#O,A#) and A5: O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1@) \/ (the Extent of CP2@))) and A6: A = (the Intent of CP1@) /\ (the Intent of CP2@) by Def18; the Extent of CP1@ c= the Extent of CP2@ by A2; then (the Extent of CP1@) \/ (the Extent of CP2@) = the Extent of CP2@ by XBOOLE_1:12; then O = (AttributeDerivation(C)).(the Intent of CP2@) by A5,Def9 .= the Extent of CP2@ by Def9; then CP1 "\/" CP2 = CP2 by A3,A4,A6,LATTICES:def 1; hence CP1 [= CP2 by LATTICES:def 3; end; now assume CP1 [= CP2; then CP1 "\/" CP2 = CP2 by LATTICES:def 3; then A7: (the L_join of CL).(CP1,CP2) = CP2 by LATTICES:def 1; ex O being Subset of the carrier of C, A being Subset of the carrier' of C st (B-join(C)).(CP1@,CP2@) = ConceptStr(#O,A#) & O = ( AttributeDerivation (C)).((ObjectDerivation(C)). ((the Extent of CP1@) \/ (the Extent of CP2@))) & A = (the Intent of CP1@) /\ (the Intent of CP2@) by Def18; then for x being object holds x in the Intent of CP2@ implies x in the Intent of CP1@ by A7,XBOOLE_0:def 4; then the Intent of CP2@ c= the Intent of CP1@; hence CP1@ is-SubConcept-of CP2@ by Th28; end; hence thesis by A1; end; theorem Th44: for C being FormalContext holds ConceptLattice(C) is complete Lattice proof let C be FormalContext; for X being Subset of ConceptLattice(C) ex a being Element of ConceptLattice(C) st a is_less_than X & for b being Element of ConceptLattice(C ) st b is_less_than X holds b [= a proof let X be Subset of ConceptLattice(C); per cases; suppose A1: X = {}; A2: for b being Element of ConceptLattice(C) st b is_less_than X holds b [= Top ConceptLattice(C) proof let b be Element of ConceptLattice(C); assume b is_less_than X; ex c being Element of ConceptLattice(C) st for a being Element of ConceptLattice(C) holds c"\/"a = c & a"\/"c = c proof reconsider CO = Concept-with-all-Objects(C) as Element of ConceptLattice(C) by Th31; for CP being Element of ConceptLattice(C) holds CO "\/" CP = CO & CP "\/" CO = CO proof let CP be Element of ConceptLattice(C); reconsider CP as strict FormalConcept of C by Th31; reconsider CO as strict FormalConcept of C; (B-join(C)).(CO,CP) = (B-join(C)).(CP,CO) by Th33 .= CO by Th39; hence thesis by LATTICES:def 1; end; hence thesis; end; then ConceptLattice(C) is upper-bounded by LATTICES:def 14; then Top ConceptLattice(C) "\/" b = Top ConceptLattice(C); hence thesis by LATTICES:def 3; end; for q being Element of ConceptLattice(C) st q in X holds Top ConceptLattice(C) [= q by A1; then Top ConceptLattice(C) is_less_than X by LATTICE3:def 16; hence thesis by A2; end; suppose X <> {}; then reconsider X as non empty Subset of ConceptLattice(C); set ExX = { the Extent of x where x is Element of B-carrier(C) : x in X }; A3: for x being Element of X holds the Extent of x in ExX proof let x be Element of X; x in X; then reconsider x as Element of B-carrier(C); the Extent of x in ExX; hence thesis; end; then reconsider ExX as non empty set; set E1 = meet ExX; A4: for o being Object of C holds o in E1 iff for x being Element of X holds o in the Extent of x proof let o be Object of C; A5: (for x being Element of X holds o in the Extent of x) implies o in E1 proof assume A6: for x being Element of X holds o in the Extent of x; for Y being set holds Y in ExX implies o in Y proof let Y be set; assume Y in ExX; then ex Y9 being Element of B-carrier(C) st Y = the Extent of Y9 & Y9 in X; hence thesis by A6; end; hence thesis by SETFAM_1:def 1; end; o in E1 implies for x being Element of X holds o in the Extent of x proof assume A7: o in E1; let x be Element of X; the Extent of x in ExX by A3; hence thesis by A7,SETFAM_1:def 1; end; hence thesis by A5; end; E1 c= the carrier of C proof set Y = the Element of ExX; let x be object; Y in ExX; then consider Y9 being Element of B-carrier(C) such that A8: Y = the Extent of Y9 and Y9 in X; assume x in E1; then x in the Extent of Y9 by A8,SETFAM_1:def 1; hence thesis; end; then consider O being Subset of the carrier of C such that A9: for o being Object of C holds o in O iff for x being Element of X holds o in the Extent of x by A4; set InX = { the Intent of x where x is Element of B-carrier(C) : x in X }; set In = union InX; A10: for a being Attribute of C holds a in In iff ex x being Element of X st a in the Intent of x proof let a be Attribute of C; A11: (ex x being Element of X st a in the Intent of x) implies a in In proof assume A12: ex x being Element of X st a in the Intent of x; ex Y being set st a in Y & Y in InX proof consider x being Element of X such that A13: a in the Intent of x by A12; x in X; then the Intent of x in InX; hence thesis by A13; end; hence thesis by TARSKI:def 4; end; a in In implies ex x being Element of X st a in the Intent of x proof assume a in In; then consider Y being set such that A14: a in Y and A15: Y in InX by TARSKI:def 4; ex Y9 being Element of B-carrier(C) st Y = the Intent of Y9 & Y9 in X by A15; hence thesis by A14; end; hence thesis by A11; end; In c= the carrier' of C proof let x be object; assume x in In; then consider Y being set such that A16: x in Y and A17: Y in InX by TARSKI:def 4; ex Y9 being Element of B-carrier(C) st Y = the Intent of Y9 & Y9 in X by A17; hence thesis by A16; end; then consider A9 being Subset of the carrier' of C such that A18: for a being Attribute of C holds a in A9 iff ex x being Element of X st a in the Intent of x by A10; A19: for o being Object of C holds o in O iff for x being Element of X holds o in (AttributeDerivation(C)).(the Intent of x) proof let o be Object of C; A20: (for x being Element of X holds o in (AttributeDerivation(C)).( the Intent of x)) implies o in O proof assume A21: for x being Element of X holds o in (AttributeDerivation(C) ).(the Intent of x); for x being Element of X holds o in the Extent of x proof let x be Element of X; o in (AttributeDerivation(C)).(the Intent of x) by A21; hence thesis by Def9; end; hence thesis by A9; end; o in O implies for x being Element of X holds o in ( AttributeDerivation(C)).(the Intent of x) proof assume A22: o in O; for x being Element of X holds o in (AttributeDerivation(C)).( the Intent of x) proof let x be Element of X; o in the Extent of x by A9,A22; hence thesis by Def9; end; hence thesis; end; hence thesis by A20; end; A23: for x being object holds x in (AttributeDerivation(C)).A9 implies x in O proof let x be object; assume x in (AttributeDerivation(C)).A9; then x in {o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a} by Def3; then consider x9 being Object of C such that A24: x9 = x and A25: for a being Attribute of C st a in A9 holds x9 is-connected-with a; for x being Element of X holds x9 in (AttributeDerivation(C)).( the Intent of x) proof let x be Element of X; for a being Attribute of C st a in (the Intent of x) holds x9 is-connected-with a by A18,A25; then x9 in {o where o is Object of C : for a being Attribute of C st a in (the Intent of x) holds o is-connected-with a}; hence thesis by Def3; end; hence thesis by A19,A24; end; consider A being Subset of the carrier' of C such that A26: A = (ObjectDerivation(C)).((AttributeDerivation(C)).A9); set p = ConceptStr(#O,A#); for x being object holds x in O implies x in (AttributeDerivation(C)). A9 proof let x9 be object; assume A27: x9 in O; then reconsider x9 as Object of C; for a being Attribute of C st a in A9 holds x9 is-connected-with a proof let a be Attribute of C; assume a in A9; then consider x being Element of X such that A28: a in the Intent of x by A18; x9 in (AttributeDerivation(C)).(the Intent of x) by A19,A27; then x9 in {o where o is Object of C : for a being Attribute of C st a in the Intent of x holds o is-connected-with a} by Def3; then ex y being Object of C st y = x9 & for a being Attribute of C st a in the Intent of x holds y is-connected-with a; hence thesis by A28; end; then x9 in {o where o is Object of C : for a being Attribute of C st a in A9 holds o is-connected-with a}; hence thesis by Def3; end; then O = (AttributeDerivation(C)).A9 by A23,TARSKI:2; then p is FormalConcept of C by A26,Th21; then reconsider p as Element of ConceptLattice(C) by Th31; A29: for b being Element of ConceptLattice(C) st b is_less_than X holds b [= p proof let b be Element of ConceptLattice(C); assume A30: b is_less_than X; the Extent of b@ c= the Extent of p@ proof let x9 be object; assume A31: x9 in the Extent of b@; then reconsider x9 as Object of C; for x being Element of X holds x9 in the Extent of x proof let x be Element of X; x in X; then reconsider x as Element of ConceptLattice(C); b [= x by A30,LATTICE3:def 16; then b@ is-SubConcept-of x@ by Th43; then the Extent of b@ c= the Extent of x@; hence thesis by A31; end; hence thesis by A9; end; then b@ is-SubConcept-of p@; hence thesis by Th43; end; for q being Element of ConceptLattice(C) st q in X holds p [= q proof let q be Element of ConceptLattice(C); assume A32: q in X; the Extent of p@ c= the Extent of q@ by A9,A32; then p@ is-SubConcept-of q@; hence thesis by Th43; end; then p is_less_than X by LATTICE3:def 16; hence thesis by A29; end; end; hence thesis by VECTSP_8:def 6; end; registration let C be FormalContext; cluster ConceptLattice(C) -> complete; coherence by Th44; end;