:: CONLAT_1 semantic presentation begin definition let C be 2-sorted ; attrC is quasi-empty means :Def1: :: CONLAT_1:def 1 ( the carrier of C is empty or the carrier' of C is empty ); end; :: deftheorem Def1 defines quasi-empty CONLAT_1:def_1_:_ for C being 2-sorted holds ( C is quasi-empty iff ( the carrier of C is empty or the carrier' of C is empty ) ); registration cluster non empty strict non void for 2-sorted ; existence ex b1 being 2-sorted st ( b1 is strict & not b1 is empty & not b1 is void ) proof ( not 2-sorted(# {{}},{{}} #) is empty & not 2-sorted(# {{}},{{}} #) is void ) ; hence ex b1 being 2-sorted st ( b1 is strict & not b1 is empty & not b1 is void ) ; ::_thesis: verum end; cluster strict non quasi-empty for 2-sorted ; existence ex b1 being 2-sorted st ( b1 is strict & not b1 is quasi-empty ) proof not 2-sorted(# {{}},{{}} #) is quasi-empty by Def1; hence ex b1 being 2-sorted st ( b1 is strict & not b1 is quasi-empty ) ; ::_thesis: verum end; end; registration cluster empty strict void quasi-empty for 2-sorted ; existence ex b1 being 2-sorted st ( b1 is strict & b1 is empty & b1 is void & b1 is quasi-empty ) proof ( 2-sorted(# {},{} #) is empty & 2-sorted(# {},{} #) is void & 2-sorted(# {},{} #) is quasi-empty ) by Def1; hence ex b1 being 2-sorted st ( b1 is strict & b1 is empty & b1 is void & b1 is quasi-empty ) ; ::_thesis: verum end; end; definition attrc1 is strict ; struct ContextStr -> 2-sorted ; aggrContextStr(# carrier, carrier', Information #) -> ContextStr ; sel Information c1 -> Relation of the carrier of c1, the carrier' of c1; end; registration cluster non empty strict for ContextStr ; existence ex b1 being ContextStr st ( b1 is strict & not b1 is empty ) proof set I = the Relation of {{}},{{}}; not ContextStr(# {{}},{{}}, the Relation of {{}},{{}} #) is empty ; hence ex b1 being ContextStr st ( b1 is strict & not b1 is empty ) ; ::_thesis: verum end; cluster non quasi-empty strict for ContextStr ; existence ex b1 being ContextStr st ( b1 is strict & not b1 is quasi-empty ) proof set I = the Relation of {{}},{{}}; not ContextStr(# {{}},{{}}, the Relation of {{}},{{}} #) is quasi-empty by Def1; hence ex b1 being ContextStr st ( b1 is strict & not b1 is quasi-empty ) ; ::_thesis: verum end; end; definition mode FormalContext is non quasi-empty 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 quasi-empty 2-sorted ; cluster the carrier' of C -> non empty ; coherence not the carrier' of C is empty by Def1; cluster the carrier of C -> non empty ; coherence not the carrier of C is empty by Def1; end; registration let C be non quasi-empty 2-sorted ; cluster non empty for Element of bool the carrier of C; existence not for b1 being Subset of the carrier of C holds b1 is empty proof take the carrier of C ; ::_thesis: ( the carrier of C is Subset of the carrier of C & not the carrier of C is empty ) the carrier of C c= the carrier of C ; hence ( the carrier of C is Subset of the carrier of C & not the carrier of C is empty ) ; ::_thesis: verum end; cluster non empty for Element of bool the carrier' of C; existence not for b1 being Subset of the carrier' of C holds b1 is empty proof take the carrier' of C ; ::_thesis: ( the carrier' of C is Subset of the carrier' of C & not the carrier' of C is empty ) the carrier' of C c= the carrier' of C ; hence ( the carrier' of C is Subset of the carrier' of C & not the carrier' of C is empty ) ; ::_thesis: verum end; end; definition let C be FormalContext; let o be Object of C; let a be Attribute of C; predo is-connected-with a means :Def2: :: CONLAT_1:def 2 [o,a] in the Information of C; end; :: deftheorem Def2 defines is-connected-with CONLAT_1:def_2_:_ for C being FormalContext for o being Object of C for a being Attribute of C holds ( o is-connected-with a iff [o,a] in the Information of C ); 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; begin definition let C be FormalContext; func ObjectDerivation C -> Function of (bool the carrier of C),(bool the carrier' of C) means :Def3: :: CONLAT_1:def 3 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 ex b1 being Function of (bool the carrier of C),(bool the carrier' of C) st for O being Subset of the carrier of C holds b1 . 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 set 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 } ] where O is Subset of the carrier of C : verum } ; for u being set st u in { [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 : verum } holds ex v, w being set st u = [v,w] proof let u be set ; ::_thesis: ( u in { [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 : verum } implies ex v, w being set st u = [v,w] ) assume u in { [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 : verum } ; ::_thesis: ex v, w being set st u = [v,w] 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 ex v, w being set st u = [v,w] ; ::_thesis: verum end; then reconsider 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 } ] where O is Subset of the carrier of C : verum } as Relation by RELAT_1:def_1; for u, v1, v2 being set st [u,v1] in f & [u,v2] in f holds v1 = v2 proof let u, v1, v2 be set ; ::_thesis: ( [u,v1] in f & [u,v2] in f implies v1 = v2 ) assume that A1: [u,v1] in f and A2: [u,v2] in f ; ::_thesis: v1 = v2 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 v1 = v2 by A4, A6; ::_thesis: verum end; then reconsider f = f as Function by FUNCT_1:def_1; A7: for x being set st x in dom f holds x in bool the carrier of C proof let x be set ; ::_thesis: ( x in dom f implies x in bool the carrier of C ) assume x in dom f ; ::_thesis: x in bool the carrier of C then consider y being set 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 x in bool the carrier of C ; ::_thesis: verum end; for x being set st x in bool the carrier of C holds x in dom f proof let x be set ; ::_thesis: ( x in bool the carrier of C implies x in dom f ) assume x in bool the carrier of C ; ::_thesis: x in dom f then reconsider x = 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 x in dom f by XTUPLE_0:def_12; ::_thesis: verum end; then A10: dom f = bool the carrier of C by A7, TARSKI:1; rng f c= bool the carrier' of C proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in bool the carrier' of C ) assume y in rng f ; ::_thesis: y in bool the carrier' of C then consider x being set 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } or u in the carrier' of C ) assume u in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } ; ::_thesis: u in the carrier' of C 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 u in the carrier' of C ; ::_thesis: verum 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 y in bool the carrier' of C by A13; ::_thesis: verum end; then reconsider f = 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 ; ::_thesis: 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 } 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; ::_thesis: 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 } consider y being set 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 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 } by A10, A14, A16, FUNCT_1:def_2; ::_thesis: verum end; hence 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 } ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (bool the carrier of C),(bool the carrier' of C) st ( for O being Subset of the carrier of C holds b1 . O = { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } ) & ( for O being Subset of the carrier of C holds b2 . O = { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } ) holds b1 = b2 proof let F1, F2 be Function of (bool the carrier of C),(bool the carrier' of C); ::_thesis: ( ( 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 } ) & ( 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 } ) implies F1 = F2 ) 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 } ; ::_thesis: ( ex O being Subset of the carrier of C st not 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 } or F1 = F2 ) 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 } ; ::_thesis: F1 = F2 A19: for O being set st O in bool the carrier of C holds F1 . O = F2 . O proof let O be set ; ::_thesis: ( O in bool the carrier of C implies F1 . O = F2 . O ) assume O in bool the carrier of C ; ::_thesis: F1 . O = F2 . O then reconsider O = 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 F1 . O = F2 . O ; ::_thesis: verum end; ( dom F1 = bool the carrier of C & dom F2 = bool the carrier of C ) by FUNCT_2:def_1; hence F1 = F2 by A19, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def3 defines ObjectDerivation CONLAT_1:def_3_:_ for C being FormalContext for b2 being Function of (bool the carrier of C),(bool the carrier' of C) holds ( b2 = ObjectDerivation C iff for O being Subset of the carrier of C holds b2 . O = { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } ); definition let C be FormalContext; func AttributeDerivation C -> Function of (bool the carrier' of C),(bool the carrier of C) means :Def4: :: CONLAT_1:def 4 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 ex b1 being Function of (bool the carrier' of C),(bool the carrier of C) st for A being Subset of the carrier' of C holds b1 . 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 set 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 } ] where A is Subset of the carrier' of C : verum } ; for u being set st u in { [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 : verum } holds ex v, w being set st u = [v,w] proof let u be set ; ::_thesis: ( u in { [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 : verum } implies ex v, w being set st u = [v,w] ) assume u in { [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 : verum } ; ::_thesis: ex v, w being set st u = [v,w] 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 ex v, w being set st u = [v,w] ; ::_thesis: verum end; then reconsider 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 } ] where A is Subset of the carrier' of C : verum } as Relation by RELAT_1:def_1; for u, v1, v2 being set st [u,v1] in f & [u,v2] in f holds v1 = v2 proof let u, v1, v2 be set ; ::_thesis: ( [u,v1] in f & [u,v2] in f implies v1 = v2 ) assume that A1: [u,v1] in f and A2: [u,v2] in f ; ::_thesis: v1 = v2 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 v1 = v2 by A4, A6; ::_thesis: verum end; then reconsider f = f as Function by FUNCT_1:def_1; A7: for x being set st x in dom f holds x in bool the carrier' of C proof let x be set ; ::_thesis: ( x in dom f implies x in bool the carrier' of C ) assume x in dom f ; ::_thesis: x in bool the carrier' of C then consider y being set 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 x in bool the carrier' of C ; ::_thesis: verum end; for x being set st x in bool the carrier' of C holds x in dom f proof let x be set ; ::_thesis: ( x in bool the carrier' of C implies x in dom f ) assume x in bool the carrier' of C ; ::_thesis: x in dom f then reconsider x = 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 x in dom f by XTUPLE_0:def_12; ::_thesis: verum end; then A10: dom f = bool the carrier' of C by A7, TARSKI:1; rng f c= bool the carrier of C proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in bool the carrier of C ) assume y in rng f ; ::_thesis: y in bool the carrier of C then consider x being set 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or u in the carrier of C ) 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 } ; ::_thesis: u in the carrier of C 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 u in the carrier of C ; ::_thesis: verum 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 y in bool the carrier of C by A13; ::_thesis: verum end; then reconsider f = 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 ; ::_thesis: 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 } 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; ::_thesis: 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 } consider y being set 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 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 } by A10, A14, A16, FUNCT_1:def_2; ::_thesis: verum end; hence 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 } ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (bool the carrier' of C),(bool the carrier of C) st ( for A being Subset of the carrier' of C holds b1 . A = { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } ) & ( for A being Subset of the carrier' of C holds b2 . A = { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } ) holds b1 = b2 proof let F1, F2 be Function of (bool the carrier' of C),(bool the carrier of C); ::_thesis: ( ( 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 } ) & ( 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 } ) implies F1 = F2 ) 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 } ; ::_thesis: ( ex A being Subset of the carrier' of C st not 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 } or F1 = F2 ) 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 } ; ::_thesis: F1 = F2 A19: for A being set st A in bool the carrier' of C holds F1 . A = F2 . A proof let A be set ; ::_thesis: ( A in bool the carrier' of C implies F1 . A = F2 . A ) assume A in bool the carrier' of C ; ::_thesis: F1 . A = F2 . A then reconsider A = 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 F1 . A = F2 . A ; ::_thesis: verum end; ( dom F1 = bool the carrier' of C & dom F2 = bool the carrier' of C ) by FUNCT_2:def_1; hence F1 = F2 by A19, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def4 defines AttributeDerivation CONLAT_1:def_4_:_ for C being FormalContext for b2 being Function of (bool the carrier' of C),(bool the carrier of C) holds ( b2 = AttributeDerivation C iff for A being Subset of the carrier' of C holds b2 . A = { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } ); theorem :: CONLAT_1:1 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; ::_thesis: for o being Object of C holds (ObjectDerivation C) . {o} = { a where a is Attribute of C : o is-connected-with a } let o be Object of C; ::_thesis: (ObjectDerivation C) . {o} = { a where a is Attribute of C : o is-connected-with a } {o} c= the carrier of C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {o} or x in the carrier of C ) assume x in {o} ; ::_thesis: x in the carrier of C then x = o by TARSKI:def_1; hence x in the carrier of C ; ::_thesis: verum end; then reconsider t = {o} as Subset of the carrier of C ; A1: for x being set st 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 } holds x in { a where a is Attribute of C : o is-connected-with a } proof set o9 = the Element of t; let x be set ; ::_thesis: ( 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 } ) reconsider o9 = the Element of t 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 } ; ::_thesis: x in { a where a is Attribute of C : o 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 = x as Attribute of C ; o9 is-connected-with x by A3; hence x in { a where a is Attribute of C : o is-connected-with a } by A2; ::_thesis: verum end; A4: for x being set st x in { a where a is Attribute of C : o is-connected-with a } 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 } proof let x be set ; ::_thesis: ( 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 } ) assume x in { a where a is Attribute of C : o is-connected-with a } ; ::_thesis: 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 A5: ex x9 being Attribute of C st ( x9 = x & o is-connected-with x9 ) ; then reconsider x = 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 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 } ; ::_thesis: verum 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 Def3; hence (ObjectDerivation C) . {o} = { a where a is Attribute of C : o is-connected-with a } by A1, A4, TARSKI:1; ::_thesis: verum end; theorem :: CONLAT_1:2 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; ::_thesis: for a being Attribute of C holds (AttributeDerivation C) . {a} = { o where o is Object of C : o is-connected-with a } let a be Attribute of C; ::_thesis: (AttributeDerivation C) . {a} = { o where o is Object of C : o is-connected-with a } {a} c= the carrier' of C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a} or x in the carrier' of C ) assume x in {a} ; ::_thesis: x in the carrier' of C then x = a by TARSKI:def_1; hence x in the carrier' of C ; ::_thesis: verum end; then reconsider t = {a} as Subset of the carrier' of C ; A1: for x being set st 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 } holds x in { o where o is Object of C : o is-connected-with a } proof set a9 = the Element of t; let x be set ; ::_thesis: ( 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 } ) reconsider a9 = the Element of t 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 } ; ::_thesis: x in { o where o is Object of C : o is-connected-with a } 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 = x as Object of C ; x is-connected-with a9 by A3; hence x in { o where o is Object of C : o is-connected-with a } by A2; ::_thesis: verum end; A4: for x being set st x in { o where o is Object of C : o is-connected-with a } 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 } proof let x be set ; ::_thesis: ( 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 } ) assume x in { o where o is Object of C : o is-connected-with a } ; ::_thesis: 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 A5: ex x9 being Object of C st ( x9 = x & x9 is-connected-with a ) ; then reconsider x = 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 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 } ; ::_thesis: verum 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 Def4; hence (AttributeDerivation C) . {a} = { o where o is Object of C : o is-connected-with a } by A1, A4, TARSKI:1; ::_thesis: verum end; theorem Th3: :: CONLAT_1:3 for C being FormalContext for O1, O2 being Subset of the carrier of C st O1 c= O2 holds (ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1 proof let C be FormalContext; ::_thesis: for O1, O2 being Subset of the carrier of C st O1 c= O2 holds (ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1 let O1, O2 be Subset of the carrier of C; ::_thesis: ( O1 c= O2 implies (ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1 ) assume A1: O1 c= O2 ; ::_thesis: (ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (ObjectDerivation C) . O2 or x in (ObjectDerivation C) . O1 ) assume x in (ObjectDerivation C) . O2 ; ::_thesis: x in (ObjectDerivation C) . O1 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 Def3; 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 x in (ObjectDerivation C) . O1 by Def3; ::_thesis: verum end; theorem Th4: :: CONLAT_1:4 for C being FormalContext for A1, A2 being Subset of the carrier' of C st A1 c= A2 holds (AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1 proof let C be FormalContext; ::_thesis: for A1, A2 being Subset of the carrier' of C st A1 c= A2 holds (AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1 let A1, A2 be Subset of the carrier' of C; ::_thesis: ( A1 c= A2 implies (AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1 ) assume A1: A1 c= A2 ; ::_thesis: (AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (AttributeDerivation C) . A2 or x in (AttributeDerivation C) . A1 ) assume x in (AttributeDerivation C) . A2 ; ::_thesis: x in (AttributeDerivation C) . A1 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 Def4; 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 x in (AttributeDerivation C) . A1 by Def4; ::_thesis: verum end; theorem Th5: :: CONLAT_1:5 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; ::_thesis: for O being Subset of the carrier of C holds O c= (AttributeDerivation C) . ((ObjectDerivation C) . O) let O be Subset of the carrier of C; ::_thesis: O c= (AttributeDerivation C) . ((ObjectDerivation C) . O) 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 set st 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 } holds x in the carrier' of C proof let x be set ; ::_thesis: ( 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 } implies x in the carrier' of C ) assume 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 } ; ::_thesis: x in the carrier' of C 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 x in the carrier' of C ; ::_thesis: verum end; then reconsider A = { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } as Subset of the carrier' of C by TARSKI:def_3; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in O or x in (AttributeDerivation C) . ((ObjectDerivation C) . O) ) assume A1: x in O ; ::_thesis: x in (AttributeDerivation C) . ((ObjectDerivation C) . O) then reconsider x = 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; ::_thesis: ( a in A implies x is-connected-with a ) assume a in A ; ::_thesis: x is-connected-with 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 x is-connected-with a by A1; ::_thesis: verum 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 Def4; then x in (AttributeDerivation C) . A by A2; hence x in (AttributeDerivation C) . ((ObjectDerivation C) . O) by Def3; ::_thesis: verum end; theorem Th6: :: CONLAT_1:6 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; ::_thesis: for A being Subset of the carrier' of C holds A c= (ObjectDerivation C) . ((AttributeDerivation C) . A) let A be Subset of the carrier' of C; ::_thesis: A c= (ObjectDerivation C) . ((AttributeDerivation C) . A) 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 set st 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 } holds x in the carrier of C proof let x be set ; ::_thesis: ( 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 } implies x in the carrier of C ) assume 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 } ; ::_thesis: x in the carrier of C 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 x in the carrier of C ; ::_thesis: verum end; then reconsider O = { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } as Subset of the carrier of C by TARSKI:def_3; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in (ObjectDerivation C) . ((AttributeDerivation C) . A) ) assume A1: x in A ; ::_thesis: x in (ObjectDerivation C) . ((AttributeDerivation C) . A) then reconsider x = 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; ::_thesis: ( o in O implies o is-connected-with x ) assume o in O ; ::_thesis: o is-connected-with x 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 o is-connected-with x by A1; ::_thesis: verum end; (ObjectDerivation C) . O = { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } by Def3; then x in (ObjectDerivation C) . O by A2; hence x in (ObjectDerivation C) . ((AttributeDerivation C) . A) by Def4; ::_thesis: verum end; theorem Th7: :: CONLAT_1:7 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; ::_thesis: for O being Subset of the carrier of C holds (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O)) let O be Subset of the carrier of C; ::_thesis: (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O)) 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 where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with 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 where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } ; A1: for x being set st x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } holds 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 } proof let x be set ; ::_thesis: ( x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } implies 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 } ) assume x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } ; ::_thesis: 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 } then A2: ex x9 being Attribute of C st ( x9 = x & ( for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with x9 ) ) ; then reconsider x = 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; ::_thesis: ( o in O implies o is-connected-with x ) assume A3: o in O ; ::_thesis: o is-connected-with x now__::_thesis:_(_(_o_in__{__o_where_o_is_Object_of_C_:_for_a_being_Attribute_of_C_st_a_in__{__a_where_a_is_Attribute_of_C_:_for_o_being_Object_of_C_st_o_in_O_holds_ o_is-connected-with_a__}__holds_ o_is-connected-with_a__}__&_o_is-connected-with_x_)_or_(_not_o_in__{__o_where_o_is_Object_of_C_:_for_a_being_Attribute_of_C_st_a_in__{__a_where_a_is_Attribute_of_C_:_for_o_being_Object_of_C_st_o_in_O_holds_ o_is-connected-with_a__}__holds_ o_is-connected-with_a__}__&_o_is-connected-with_x_)_) percases ( o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } or not o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } ) ; case o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } ; ::_thesis: o is-connected-with x hence o is-connected-with x by A2; ::_thesis: verum end; case not o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } ; ::_thesis: o is-connected-with x then consider a being Attribute of C such that A4: a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with 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 o is-connected-with x by A3, A5; ::_thesis: verum end; end; end; hence o is-connected-with x ; ::_thesis: verum end; hence 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 } ; ::_thesis: verum end; for x being set st 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 } holds x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } proof let x be set ; ::_thesis: ( 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 } implies x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } ) assume A6: 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 } ; ::_thesis: x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with 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 = x as Attribute of C ; for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with x proof let o be Object of C; ::_thesis: ( o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } implies o is-connected-with x ) assume o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } ; ::_thesis: o is-connected-with x then ex o9 being Object of C st ( o9 = o & ( for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o9 is-connected-with a ) ) ; hence o is-connected-with x by A6; ::_thesis: verum end; hence x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } ; ::_thesis: verum end; then A7: { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } = { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } by A1, TARSKI:1; { 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 x be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in the carrier' of C ) assume 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 } ; ::_thesis: x in the carrier' of C 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 x in the carrier' of C ; ::_thesis: verum end; then reconsider A = { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } as Subset of the carrier' of C ; { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } c= the carrier of C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } or x in the carrier of C ) assume x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } ; ::_thesis: x in the carrier of C 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 x in the carrier of C ; ::_thesis: verum end; then reconsider O9 = { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds o is-connected-with a } holds o is-connected-with a } as Subset of the carrier of C ; ( A = (ObjectDerivation C) . O & O9 = (AttributeDerivation C) . A ) by Def3, Def4; hence (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O)) by A7, Def3; ::_thesis: verum end; theorem Th8: :: CONLAT_1:8 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; ::_thesis: for A being Subset of the carrier' of C holds (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A)) let A be Subset of the carrier' of C; ::_thesis: (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A)) 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 where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } 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 where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } ; A1: for x being set st x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } holds 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 } proof let x be set ; ::_thesis: ( x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } implies 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 } ) assume x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } ; ::_thesis: 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 } then A2: ex x9 being Object of C st ( x9 = x & ( for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } holds x9 is-connected-with a ) ) ; then reconsider x = 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; ::_thesis: ( a in A implies x is-connected-with a ) assume A3: a in A ; ::_thesis: x is-connected-with a now__::_thesis:_(_(_a_in__{__a_where_a_is_Attribute_of_C_:_for_o_being_Object_of_C_st_o_in__{__o_where_o_is_Object_of_C_:_for_a_being_Attribute_of_C_st_a_in_A_holds_ o_is-connected-with_a__}__holds_ o_is-connected-with_a__}__&_x_is-connected-with_a_)_or_(_not_a_in__{__a_where_a_is_Attribute_of_C_:_for_o_being_Object_of_C_st_o_in__{__o_where_o_is_Object_of_C_:_for_a_being_Attribute_of_C_st_a_in_A_holds_ o_is-connected-with_a__}__holds_ o_is-connected-with_a__}__&_x_is-connected-with_a_)_) percases ( a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } or not a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } ) ; case a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } ; ::_thesis: x is-connected-with a hence x is-connected-with a by A2; ::_thesis: verum end; case not a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } ; ::_thesis: x is-connected-with a then consider o being Object of C such that A4: o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } 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 x is-connected-with a by A3, A5; ::_thesis: verum end; end; end; hence x is-connected-with a ; ::_thesis: verum end; hence 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 } ; ::_thesis: verum end; for x being set st 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 } holds x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } proof let x be set ; ::_thesis: ( 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 } implies x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } ) assume 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 } ; ::_thesis: x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } 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 = x as Object of C ; for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } holds x is-connected-with a proof let a be Attribute of C; ::_thesis: ( a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } implies x is-connected-with a ) assume a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } ; ::_thesis: x is-connected-with a then ex a9 being Attribute of C st ( a9 = a & ( for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a9 ) ) ; hence x is-connected-with a by A6; ::_thesis: verum end; hence x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } ; ::_thesis: verum end; then A7: { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } = { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } holds o is-connected-with a } by A1, TARSKI:1; { 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 x be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in the carrier of C ) assume 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 } ; ::_thesis: x in the carrier of C 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 x in the carrier of C ; ::_thesis: verum end; then reconsider O = { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } as Subset of the carrier of C ; { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } c= the carrier' of C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } or x in the carrier' of C ) assume x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } ; ::_thesis: x in the carrier' of C 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 x in the carrier' of C ; ::_thesis: verum end; then reconsider A9 = { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds o is-connected-with a } holds o is-connected-with a } as Subset of the carrier' of C ; ( O = (AttributeDerivation C) . A & A9 = (ObjectDerivation C) . O ) by Def3, Def4; hence (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A)) by A7, Def4; ::_thesis: verum end; theorem Th9: :: CONLAT_1:9 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; ::_thesis: 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 ) let O be Subset of the carrier of C; ::_thesis: for A being Subset of the carrier' of C holds ( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C ) let A be Subset of the carrier' of C; ::_thesis: ( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information 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 ; ::_thesis: O c= (AttributeDerivation C) . A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in O or x in (AttributeDerivation C) . A ) assume A3: x in O ; ::_thesis: x in (AttributeDerivation C) . A then reconsider x = 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; ::_thesis: ( a in A implies x is-connected-with a ) consider z being set such that A4: z = [x,a] ; assume a in A ; ::_thesis: x is-connected-with a then z in [:O,A:] by A3, A4, ZFMISC_1:def_2; hence x is-connected-with a by A2, A4, Def2; ::_thesis: verum 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 x in (AttributeDerivation C) . A by Def4; ::_thesis: verum end; ( O c= (AttributeDerivation C) . A implies [:O,A:] c= the Information of C ) proof assume O c= (AttributeDerivation C) . A ; ::_thesis: [:O,A:] c= the Information of C 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 Def4; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:O,A:] or z in the Information of C ) assume z in [:O,A:] ; ::_thesis: z in the Information of C then consider x, y being set such that A6: x in O and A7: y in A and A8: z = [x,y] by ZFMISC_1:def_2; reconsider y = y as Attribute of C by A7; reconsider x = 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 z in the Information of C by A8, Def2; ::_thesis: verum end; hence ( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C ) by A1; ::_thesis: verum end; theorem Th10: :: CONLAT_1:10 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; ::_thesis: 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 ) let O be Subset of the carrier of C; ::_thesis: for A being Subset of the carrier' of C holds ( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information of C ) let A be Subset of the carrier' of C; ::_thesis: ( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information 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 ; ::_thesis: A c= (ObjectDerivation C) . O let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in (ObjectDerivation C) . O ) assume A3: x in A ; ::_thesis: x in (ObjectDerivation C) . O then reconsider x = 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; ::_thesis: ( o in O implies o is-connected-with x ) consider z being set such that A4: z = [o,x] ; assume o in O ; ::_thesis: o is-connected-with x then z in [:O,A:] by A3, A4, ZFMISC_1:def_2; hence o is-connected-with x by A2, A4, Def2; ::_thesis: verum 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 x in (ObjectDerivation C) . O by Def3; ::_thesis: verum end; ( A c= (ObjectDerivation C) . O implies [:O,A:] c= the Information of C ) proof assume A c= (ObjectDerivation C) . O ; ::_thesis: [:O,A:] c= the Information of C 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 Def3; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:O,A:] or z in the Information of C ) assume z in [:O,A:] ; ::_thesis: z in the Information of C then consider x, y being set such that A6: x in O and A7: y in A and A8: z = [x,y] by ZFMISC_1:def_2; reconsider y = y as Attribute of C by A7; reconsider x = 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 z in the Information of C by A8, Def2; ::_thesis: verum end; hence ( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information of C ) by A1; ::_thesis: verum end; theorem :: CONLAT_1:11 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; ::_thesis: 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 ) let O be Subset of the carrier of C; ::_thesis: for A being Subset of the carrier' of C holds ( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O ) let A be Subset of the carrier' of C; ::_thesis: ( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O ) ( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C ) by Th9; hence ( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O ) by Th10; ::_thesis: verum end; definition let C be FormalContext; func phi C -> Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C) equals :: CONLAT_1:def 5 ObjectDerivation C; coherence ObjectDerivation C is Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C) proof A1: rng (ObjectDerivation C) c= the carrier of (BoolePoset the carrier' of C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (ObjectDerivation C) or x in the carrier of (BoolePoset the carrier' of C) ) assume x in rng (ObjectDerivation C) ; ::_thesis: x in the carrier of (BoolePoset the carrier' of 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 x in the carrier of (BoolePoset the carrier' of C) by A2, YELLOW_1:def_2; ::_thesis: verum 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 set st x in the carrier of (BoolePoset the carrier of C) holds x in dom (ObjectDerivation C) proof let x be set ; ::_thesis: ( x in the carrier of (BoolePoset the carrier of C) implies x in dom (ObjectDerivation C) ) assume x in the carrier of (BoolePoset the carrier of C) ; ::_thesis: x in dom (ObjectDerivation 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 x in dom (ObjectDerivation C) by FUNCT_2:def_1; ::_thesis: verum end; for x being set st x in dom (ObjectDerivation C) holds x in the carrier of (BoolePoset the carrier of C) proof let x be set ; ::_thesis: ( x in dom (ObjectDerivation C) implies x in the carrier of (BoolePoset the carrier of C) ) assume x in dom (ObjectDerivation C) ; ::_thesis: x in the carrier of (BoolePoset the carrier of 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 x in the carrier of (BoolePoset the carrier of C) by A3, YELLOW_1:def_2; ::_thesis: verum end; then dom (ObjectDerivation C) = the carrier of (BoolePoset the carrier of C) by A4, TARSKI:1; 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 ObjectDerivation C is Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C) ; ::_thesis: verum end; end; :: deftheorem defines phi CONLAT_1:def_5_:_ for C being FormalContext holds phi C = ObjectDerivation C; definition let C be FormalContext; func psi C -> Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C) equals :: CONLAT_1:def 6 AttributeDerivation C; coherence AttributeDerivation C is Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C) proof A1: rng (AttributeDerivation C) c= the carrier of (BoolePoset the carrier of C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (AttributeDerivation C) or x in the carrier of (BoolePoset the carrier of C) ) assume x in rng (AttributeDerivation C) ; ::_thesis: x in the carrier of (BoolePoset the carrier of 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 x in the carrier of (BoolePoset the carrier of C) by A2, YELLOW_1:def_2; ::_thesis: verum 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 set st x in the carrier of (BoolePoset the carrier' of C) holds x in dom (AttributeDerivation C) proof let x be set ; ::_thesis: ( x in the carrier of (BoolePoset the carrier' of C) implies x in dom (AttributeDerivation C) ) assume x in the carrier of (BoolePoset the carrier' of C) ; ::_thesis: x in dom (AttributeDerivation 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 x in dom (AttributeDerivation C) by FUNCT_2:def_1; ::_thesis: verum end; for x being set st x in dom (AttributeDerivation C) holds x in the carrier of (BoolePoset the carrier' of C) proof let x be set ; ::_thesis: ( x in dom (AttributeDerivation C) implies x in the carrier of (BoolePoset the carrier' of C) ) assume x in dom (AttributeDerivation C) ; ::_thesis: x in the carrier of (BoolePoset the carrier' of 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 x in the carrier of (BoolePoset the carrier' of C) by A3, YELLOW_1:def_2; ::_thesis: verum end; then dom (AttributeDerivation C) = the carrier of (BoolePoset the carrier' of C) by A4, TARSKI:1; hence AttributeDerivation C is Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C) by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; end; :: deftheorem defines psi CONLAT_1:def_6_:_ for C being FormalContext holds psi C = AttributeDerivation C; definition let P, R be non empty RelStr ; let Con be Connection of P,R; attrCon is co-Galois means :Def7: :: CONLAT_1:def 7 ex f being Function of P,R ex g being Function of R,P st ( Con = [f,g] & f is antitone & g is antitone & ( for p1, p2 being Element of P for r1, r2 being Element of R holds ( p1 <= g . (f . p1) & r1 <= f . (g . r1) ) ) ); end; :: deftheorem Def7 defines co-Galois CONLAT_1:def_7_:_ for P, R being non empty RelStr for Con being Connection of P,R holds ( Con is co-Galois iff ex f being Function of P,R ex g being Function of R,P st ( Con = [f,g] & f is antitone & g is antitone & ( for p1, p2 being Element of P for r1, r2 being Element of R holds ( p1 <= g . (f . p1) & r1 <= f . (g . r1) ) ) ) ); theorem Th12: :: CONLAT_1:12 for P, R being non empty Poset for Con being Connection of P,R for f being Function of P,R for g being Function of R,P st Con = [f,g] holds ( Con is co-Galois iff for p being Element of P for r being Element of R holds ( p <= g . r iff r <= f . p ) ) proof let P, R be non empty Poset; ::_thesis: for Con being Connection of P,R for f being Function of P,R for g being Function of R,P st Con = [f,g] holds ( Con is co-Galois iff for p being Element of P for r being Element of R holds ( p <= g . r iff r <= f . p ) ) let Con be Connection of P,R; ::_thesis: for f being Function of P,R for g being Function of R,P st Con = [f,g] holds ( Con is co-Galois iff for p being Element of P for r being Element of R holds ( p <= g . r iff r <= f . p ) ) let f be Function of P,R; ::_thesis: for g being Function of R,P st Con = [f,g] holds ( Con is co-Galois iff for p being Element of P for r being Element of R holds ( p <= g . r iff r <= f . p ) ) let g be Function of R,P; ::_thesis: ( Con = [f,g] implies ( Con is co-Galois iff for p being Element of P for r being Element of R holds ( p <= g . r iff r <= f . p ) ) ) assume A1: Con = [f,g] ; ::_thesis: ( Con is co-Galois iff for p being Element of P for r being Element of R holds ( p <= g . r iff r <= f . p ) ) A2: now__::_thesis:_(_(_for_p_being_Element_of_P for_r_being_Element_of_R_holds_ (_p_<=_g_._r_iff_r_<=_f_._p_)_)_implies_Con_is_co-Galois_) assume A3: for p being Element of P for r being Element of R holds ( p <= g . r iff r <= f . p ) ; ::_thesis: Con is co-Galois for p1, p2 being Element of P st p1 <= p2 holds 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; ::_thesis: ( p1 <= p2 implies for r1, r2 being Element of R st r1 = f . p1 & r2 = f . p2 holds r1 >= r2 ) assume A4: p1 <= p2 ; ::_thesis: for r1, r2 being Element of R st r1 = f . p1 & r2 = f . p2 holds r1 >= r2 let r1, r2 be Element of R; ::_thesis: ( r1 = f . p1 & r2 = f . p2 implies r1 >= r2 ) assume A5: ( r1 = f . p1 & r2 = f . p2 ) ; ::_thesis: r1 >= r2 p2 <= g . (f . p2) by A3; then p1 <= g . (f . p2) by A4, ORDERS_2:3; hence r1 >= r2 by A3, A5; ::_thesis: verum end; then A6: f is antitone by WAYBEL_0:def_5; for r1, r2 being Element of R st r1 <= r2 holds 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; ::_thesis: ( r1 <= r2 implies for p1, p2 being Element of P st p1 = g . r1 & p2 = g . r2 holds p1 >= p2 ) assume A7: r1 <= r2 ; ::_thesis: for p1, p2 being Element of P st p1 = g . r1 & p2 = g . r2 holds p1 >= p2 let p1, p2 be Element of P; ::_thesis: ( p1 = g . r1 & p2 = g . r2 implies p1 >= p2 ) assume A8: ( p1 = g . r1 & p2 = g . r2 ) ; ::_thesis: p1 >= p2 r2 <= f . (g . r2) by A3; then r1 <= f . (g . r2) by A7, ORDERS_2:3; hence p1 >= p2 by A3, A8; ::_thesis: verum end; then A9: g is antitone by WAYBEL_0:def_5; for p1, p2 being Element of P for 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, Def7; ::_thesis: verum end; now__::_thesis:_(_Con_is_co-Galois_implies_for_p_being_Element_of_P for_r_being_Element_of_R_holds_ (_p_<=_g_._r_iff_r_<=_f_._p_)_) assume Con is co-Galois ; ::_thesis: for p being Element of P for r being Element of R holds ( p <= g . r iff r <= f . p ) 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 for r1, r2 being Element of R holds ( p1 <= g9 . (f9 . p1) & r1 <= f9 . (g9 . r1) ) by Def7; 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 for r being Element of R st r <= f . p holds p <= g . r proof let p be Element of P; ::_thesis: for r being Element of R st r <= f . p holds p <= g . r let r be Element of R; ::_thesis: ( r <= f . p implies p <= g . r ) assume r <= f . p ; ::_thesis: p <= g . r then A17: g . r >= g . (f . p) by A12, A14, WAYBEL_0:def_5; p <= g . (f . p) by A13, A15, A14; hence p <= g . r by A17, ORDERS_2:3; ::_thesis: verum end; for p being Element of P for r being Element of R st p <= g . r holds r <= f . p proof let p be Element of P; ::_thesis: for r being Element of R st p <= g . r holds r <= f . p let r be Element of R; ::_thesis: ( p <= g . r implies r <= f . p ) assume p <= g . r ; ::_thesis: r <= f . p then A18: f . p >= f . (g . r) by A11, A15, WAYBEL_0:def_5; r <= f . (g . r) by A13, A15, A14; hence r <= f . p by A18, ORDERS_2:3; ::_thesis: verum end; hence for p being Element of P for r being Element of R holds ( p <= g . r iff r <= f . p ) by A16; ::_thesis: verum end; hence ( Con is co-Galois iff for p being Element of P for r being Element of R holds ( p <= g . r iff r <= f . p ) ) by A2; ::_thesis: verum end; theorem :: CONLAT_1:13 for P, R being non empty Poset for Con being Connection of P,R st Con is co-Galois holds for f being Function of P,R for 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; ::_thesis: for Con being Connection of P,R st Con is co-Galois holds for f being Function of P,R for g being Function of R,P st Con = [f,g] holds ( f = f * (g * f) & g = g * (f * g) ) let Con be Connection of P,R; ::_thesis: ( Con is co-Galois implies for f being Function of P,R for g being Function of R,P st Con = [f,g] holds ( f = f * (g * f) & g = g * (f * g) ) ) assume Con is co-Galois ; ::_thesis: for f being Function of P,R for g being Function of R,P st Con = [f,g] holds ( f = f * (g * f) & g = g * (f * g) ) 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 for r1, r2 being Element of R holds ( p1 <= g9 . (f9 . p1) & r1 <= f9 . (g9 . r1) ) by Def7; let f be Function of P,R; ::_thesis: for g being Function of R,P st Con = [f,g] holds ( f = f * (g * f) & g = g * (f * g) ) let g be Function of R,P; ::_thesis: ( Con = [f,g] implies ( f = f * (g * f) & g = g * (f * g) ) ) assume A5: Con = [f,g] ; ::_thesis: ( f = f * (g * f) & g = g * (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 set st x in the carrier of P holds f . x = (f * (g * f)) . x proof let x be set ; ::_thesis: ( x in the carrier of P implies f . x = (f * (g * f)) . x ) assume x in the carrier of P ; ::_thesis: f . x = (f * (g * f)) . x then reconsider x = 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 f . x = (f * (g * f)) . x by A12, FUNCT_1:13; ::_thesis: verum end; A13: for x being set st x in the carrier of R holds g . x = (g * (f * g)) . x proof let x be set ; ::_thesis: ( x in the carrier of R implies g . x = (g * (f * g)) . x ) assume x in the carrier of R ; ::_thesis: g . x = (g * (f * g)) . x then reconsider x = 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 g . x = (g * (f * g)) . x by A15, FUNCT_1:13; ::_thesis: verum end; ( dom (f * (g * f)) = the carrier of P & dom (g * (f * g)) = the carrier of R ) by FUNCT_2:def_1; hence ( f = f * (g * f) & g = g * (f * g) ) by A9, A8, A10, A13, FUNCT_1:2; ::_thesis: verum end; theorem :: CONLAT_1:14 for C being FormalContext holds [(phi C),(psi C)] is co-Galois proof let C be FormalContext; ::_thesis: [(phi C),(psi C)] is co-Galois 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) for 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); ::_thesis: for y being Element of (BoolePoset the carrier' of C) st y <= (phi C) . x holds x <= (psi C) . y let y be Element of (BoolePoset the carrier' of C); ::_thesis: ( y <= (phi C) . x implies x <= (psi C) . y ) assume y <= (phi C) . x ; ::_thesis: x <= (psi C) . y 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 = x as Element of (BooleLatt the carrier of C) by A2, YELLOW_1:def_2; reconsider x = x as Subset of the carrier of C by LATTICE3:def_1; reconsider y = 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 = x9 as Subset of the carrier' of C by LATTICE3:def_1; reconsider y = y as Subset of the carrier' of C by LATTICE3:def_1; for z being set st z in y holds z in x9 by A5, XBOOLE_0:def_3; then y c= x9 by TARSKI:def_3; then A6: (AttributeDerivation C) . x9 c= (AttributeDerivation C) . y by Th4; reconsider y = 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 = y9 as Subset of the carrier of C by LATTICE3:def_1; reconsider y9 = y9 as Element of (BooleLatt the carrier of C) ; A7: x c= (AttributeDerivation C) . ((ObjectDerivation C) . x) by Th5; reconsider x = x as Subset of the carrier of C ; reconsider x = x as Element of (BooleLatt the carrier of C) ; x "\/" y9 = y9 by A6, A7, XBOOLE_1:1, XBOOLE_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 x <= (psi C) . y by ORDERS_2:def_5; ::_thesis: verum end; for x being Element of (BoolePoset the carrier of C) for 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); ::_thesis: for y being Element of (BoolePoset the carrier' of C) st x <= (psi C) . y holds y <= (phi C) . x let y be Element of (BoolePoset the carrier' of C); ::_thesis: ( x <= (psi C) . y implies y <= (phi C) . x ) assume x <= (psi C) . y ; ::_thesis: y <= (phi C) . x 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 = y as Element of (BooleLatt the carrier' of C) by A1, YELLOW_1:def_2; reconsider y = y as Subset of the carrier' of C by LATTICE3:def_1; reconsider x = 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 = y9 as Subset of the carrier of C by LATTICE3:def_1; reconsider x = x as Subset of the carrier of C by LATTICE3:def_1; for z being set st z in x holds z in y9 by A9, XBOOLE_0:def_3; then A10: x c= y9 by TARSKI:def_3; reconsider x = x, y9 = y9 as Subset of the carrier of C ; A11: (ObjectDerivation C) . y9 c= (ObjectDerivation C) . x by A10, Th3; reconsider x = 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 = x9 as Subset of the carrier' of C by LATTICE3:def_1; reconsider x9 = x9 as Element of (BooleLatt the carrier' of C) ; A12: y c= (ObjectDerivation C) . ((AttributeDerivation C) . y) by Th6; reconsider y = y as Element of (BooleLatt the carrier' of C) ; y "\/" x9 = x9 by A11, A12, XBOOLE_1:1, XBOOLE_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 y <= (phi C) . x by ORDERS_2:def_5; ::_thesis: verum end; hence [(phi C),(psi C)] is co-Galois by A3, Th12; ::_thesis: verum end; theorem Th15: :: CONLAT_1:15 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; ::_thesis: for O1, O2 being Subset of the carrier of C holds (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) let O1, O2 be Subset of the carrier of C; ::_thesis: (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) reconsider O9 = O1 \/ O2 as Subset of the carrier of C ; A1: for x being set st x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) holds x in (ObjectDerivation C) . O9 proof let x be set ; ::_thesis: ( x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) implies x in (ObjectDerivation C) . O9 ) assume A2: x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) ; ::_thesis: x in (ObjectDerivation C) . O9 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 Def3; 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 Def3; 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 = 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; ::_thesis: ( o in O1 \/ O2 implies o is-connected-with x ) assume A5: o in O1 \/ O2 ; ::_thesis: o is-connected-with x now__::_thesis:_(_(_o_in_O1_&_o_is-connected-with_x_)_or_(_o_in_O2_&_o_is-connected-with_x_)_) percases ( o in O1 or o in O2 ) by A5, XBOOLE_0:def_3; case o in O1 ; ::_thesis: o is-connected-with x hence o is-connected-with x by A3; ::_thesis: verum end; case o in O2 ; ::_thesis: o is-connected-with x hence o is-connected-with x by A4; ::_thesis: verum end; end; end; hence o is-connected-with x ; ::_thesis: verum 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 x in (ObjectDerivation C) . O9 by Def3; ::_thesis: verum end; for x being set st x in (ObjectDerivation C) . (O1 \/ O2) holds x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) proof let x be set ; ::_thesis: ( x in (ObjectDerivation C) . (O1 \/ O2) implies x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) ) assume x in (ObjectDerivation C) . (O1 \/ O2) ; ::_thesis: x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . 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 Def3; 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 = 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; ::_thesis: ( o in O2 implies o is-connected-with x ) assume o in O2 ; ::_thesis: o is-connected-with x then o in O9 by XBOOLE_0:def_3; hence o is-connected-with x by A6; ::_thesis: verum 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 Def3; for o being Object of C st o in O1 holds o is-connected-with x proof let o be Object of C; ::_thesis: ( o in O1 implies o is-connected-with x ) assume o in O1 ; ::_thesis: o is-connected-with x then o in O9 by XBOOLE_0:def_3; hence o is-connected-with x by A6; ::_thesis: verum 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 Def3; hence x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) by A7, XBOOLE_0:def_4; ::_thesis: verum end; hence (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) by A1, TARSKI:1; ::_thesis: verum end; theorem Th16: :: CONLAT_1:16 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; ::_thesis: for A1, A2 being Subset of the carrier' of C holds (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) let A1, A2 be Subset of the carrier' of C; ::_thesis: (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) reconsider A9 = A1 \/ A2 as Subset of the carrier' of C ; A1: for x being set st x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) holds x in (AttributeDerivation C) . A9 proof let x be set ; ::_thesis: ( x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) implies x in (AttributeDerivation C) . A9 ) assume A2: x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) ; ::_thesis: x in (AttributeDerivation C) . A9 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 Def4; 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 Def4; 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 = 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; ::_thesis: ( a in A1 \/ A2 implies x is-connected-with a ) assume A5: a in A1 \/ A2 ; ::_thesis: x is-connected-with a now__::_thesis:_(_(_a_in_A1_&_x_is-connected-with_a_)_or_(_a_in_A2_&_x_is-connected-with_a_)_) percases ( a in A1 or a in A2 ) by A5, XBOOLE_0:def_3; case a in A1 ; ::_thesis: x is-connected-with a hence x is-connected-with a by A3; ::_thesis: verum end; case a in A2 ; ::_thesis: x is-connected-with a hence x is-connected-with a by A4; ::_thesis: verum end; end; end; hence x is-connected-with a ; ::_thesis: verum 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 x in (AttributeDerivation C) . A9 by Def4; ::_thesis: verum end; for x being set st x in (AttributeDerivation C) . (A1 \/ A2) holds x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) proof let x be set ; ::_thesis: ( x in (AttributeDerivation C) . (A1 \/ A2) implies x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) ) assume x in (AttributeDerivation C) . (A1 \/ A2) ; ::_thesis: x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . 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 Def4; 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 = 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; ::_thesis: ( a in A2 implies x is-connected-with a ) assume a in A2 ; ::_thesis: x is-connected-with a then a in A9 by XBOOLE_0:def_3; hence x is-connected-with a by A6; ::_thesis: verum 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 Def4; for a being Attribute of C st a in A1 holds x is-connected-with a proof let a be Attribute of C; ::_thesis: ( a in A1 implies x is-connected-with a ) assume a in A1 ; ::_thesis: x is-connected-with a then a in A9 by XBOOLE_0:def_3; hence x is-connected-with a by A6; ::_thesis: verum 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 Def4; hence x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) by A7, XBOOLE_0:def_4; ::_thesis: verum end; hence (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) by A1, TARSKI:1; ::_thesis: verum end; theorem Th17: :: CONLAT_1:17 for C being FormalContext holds (ObjectDerivation C) . {} = the carrier' of C proof let C be FormalContext; ::_thesis: (ObjectDerivation C) . {} = the carrier' of C 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 set st x in { a where a is Attribute of C : for o being Object of C st o in e holds o is-connected-with a } holds x in the carrier' of C proof let x be set ; ::_thesis: ( x in { a where a is Attribute of C : for o being Object of C st o in e holds o is-connected-with a } implies x in the carrier' of C ) assume x in { a where a is Attribute of C : for o being Object of C st o in e holds o is-connected-with a } ; ::_thesis: x in the carrier' of C 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 x in the carrier' of C ; ::_thesis: verum end; A2: for x being set st x in the carrier' of C holds x in { a where a is Attribute of C : for o being Object of C st o in e holds o is-connected-with a } proof let x be set ; ::_thesis: ( x in the carrier' of C implies x in { a where a is Attribute of C : for o being Object of C st o in e holds o is-connected-with a } ) assume x in the carrier' of C ; ::_thesis: x in { a where a is Attribute of C : for o being Object of C st o in e holds o is-connected-with a } then reconsider x = x as Attribute of C ; for o being Object of C st o in e holds o is-connected-with x ; hence x in { a where a is Attribute of C : for o being Object of C st o in e holds o is-connected-with a } ; ::_thesis: verum 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 Def3; hence (ObjectDerivation C) . {} = the carrier' of C by A1, A2, TARSKI:1; ::_thesis: verum end; theorem Th18: :: CONLAT_1:18 for C being FormalContext holds (AttributeDerivation C) . {} = the carrier of C proof let C be FormalContext; ::_thesis: (AttributeDerivation C) . {} = the carrier of C 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 set st x in { o where o is Object of C : for a being Attribute of C st a in e holds o is-connected-with a } holds x in the carrier of C proof let x be set ; ::_thesis: ( x in { o where o is Object of C : for a being Attribute of C st a in e holds o is-connected-with a } implies x in the carrier of C ) assume x in { o where o is Object of C : for a being Attribute of C st a in e holds o is-connected-with a } ; ::_thesis: x in the carrier of C 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 x in the carrier of C ; ::_thesis: verum end; A2: for x being set st x in the carrier of C holds x in { o where o is Object of C : for a being Attribute of C st a in e holds o is-connected-with a } proof let x be set ; ::_thesis: ( x in the carrier of C implies x in { o where o is Object of C : for a being Attribute of C st a in e holds o is-connected-with a } ) assume x in the carrier of C ; ::_thesis: x in { o where o is Object of C : for a being Attribute of C st a in e holds o is-connected-with a } then reconsider x = x as Object of C ; for a being Attribute of C st a in e holds x is-connected-with a ; hence x in { o where o is Object of C : for a being Attribute of C st a in e holds o is-connected-with a } ; ::_thesis: verum 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 Def4; hence (AttributeDerivation C) . {} = the carrier of C by A1, A2, TARSKI:1; ::_thesis: verum end; begin definition let C be 2-sorted ; attrc2 is strict ; struct ConceptStr over C -> ; aggrConceptStr(# Extent, Intent #) -> ConceptStr over C; sel Extent c2 -> Subset of the carrier of C; sel Intent c2 -> Subset of the carrier' of C; end; definition let C be 2-sorted ; let CP be ConceptStr over C; attrCP is empty means :Def8: :: CONLAT_1:def 8 ( the Extent of CP is empty & the Intent of CP is empty ); attrCP is quasi-empty means :Def9: :: CONLAT_1:def 9 ( the Extent of CP is empty or the Intent of CP is empty ); end; :: deftheorem Def8 defines empty CONLAT_1:def_8_:_ for C being 2-sorted for CP being ConceptStr over C holds ( CP is empty iff ( the Extent of CP is empty & the Intent of CP is empty ) ); :: deftheorem Def9 defines quasi-empty CONLAT_1:def_9_:_ for C being 2-sorted for CP being ConceptStr over C holds ( CP is quasi-empty iff ( the Extent of CP is empty or the Intent of CP is empty ) ); registration let C be non quasi-empty 2-sorted ; cluster strict non empty for ConceptStr over C; existence ex b1 being ConceptStr over C st ( b1 is strict & not b1 is empty ) proof set A = the non empty Subset of the carrier' of C; set O = the non empty Subset of the carrier of C; not ConceptStr(# the non empty Subset of the carrier of C, the non empty Subset of the carrier' of C #) is empty by Def8; hence ex b1 being ConceptStr over C st ( b1 is strict & not b1 is empty ) ; ::_thesis: verum end; cluster strict quasi-empty for ConceptStr over C; existence ex b1 being ConceptStr over C st ( b1 is strict & b1 is quasi-empty ) 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 by Def9; hence ex b1 being ConceptStr over C st ( b1 is strict & b1 is quasi-empty ) ; ::_thesis: verum end; end; registration let C be empty void 2-sorted ; cluster -> empty for ConceptStr over C; coherence for b1 being ConceptStr over C holds b1 is empty proof let CP be ConceptStr over C; ::_thesis: CP is empty ( the Extent of CP is empty & the Intent of CP is empty ) ; hence CP is empty by Def8; ::_thesis: verum end; end; registration let C be quasi-empty 2-sorted ; cluster -> quasi-empty for ConceptStr over C; coherence for b1 being ConceptStr over C holds b1 is quasi-empty proof let CP be ConceptStr over C; ::_thesis: CP is quasi-empty ( the Extent of CP is empty or the Intent of CP is empty ) proof set x = the Element of the Extent of CP; assume not the Extent of CP is empty ; ::_thesis: the Intent of CP is empty then A1: the Element of the Extent of CP in the Extent of CP ; thus the Intent of CP is empty ::_thesis: verum proof set x = the Element of the Intent of CP; assume not the Intent of CP is empty ; ::_thesis: contradiction then the Element of the Intent of CP in the Intent of CP ; hence contradiction by A1, Def1; ::_thesis: verum end; end; hence CP is quasi-empty by Def9; ::_thesis: verum end; end; Lm1: for C being FormalContext for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds not CS is empty proof let C be FormalContext; ::_thesis: for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds not CS is empty let CS be ConceptStr over C; ::_thesis: ( (ObjectDerivation C) . the Extent of CS = the Intent of CS implies not CS is empty ) assume A1: (ObjectDerivation C) . the Extent of CS = the Intent of CS ; ::_thesis: not CS is empty now__::_thesis:_(_(_the_Extent_of_CS_is_empty_&_not_CS_is_empty_)_or_(_not_the_Extent_of_CS_is_empty_&_not_CS_is_empty_)_) percases ( the Extent of CS is empty or not the Extent of CS is empty ) ; case the Extent of CS is empty ; ::_thesis: not CS is empty then the Intent of CS = the carrier' of C by A1, Th17; hence not CS is empty by Def8; ::_thesis: verum end; case not the Extent of CS is empty ; ::_thesis: not CS is empty hence not CS is empty by Def8; ::_thesis: verum end; end; end; hence not CS is empty ; ::_thesis: verum end; definition let C be FormalContext; let CP be ConceptStr over C; attrCP is concept-like means :Def10: :: CONLAT_1:def 10 ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ); end; :: deftheorem Def10 defines concept-like CONLAT_1:def_10_:_ for C being FormalContext for CP being ConceptStr over C holds ( CP is concept-like iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) ); registration let C be FormalContext; cluster non empty concept-like for ConceptStr over C; existence ex b1 being ConceptStr over C st ( b1 is concept-like & not b1 is empty ) proof set o = the Object of C; set A = (ObjectDerivation C) . { the Object of C}; { the Object of C} c= the carrier of C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { the Object of C} or x in the carrier of C ) assume x in { the Object of C} ; ::_thesis: x in the carrier of C then x = the Object of C by TARSKI:def_1; hence x in the carrier of C ; ::_thesis: verum end; then reconsider t = { the Object of C} as Subset of the carrier of C ; (ObjectDerivation C) . { the Object of C} c= the carrier' of C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (ObjectDerivation C) . { the Object of C} or x in the carrier' of C ) assume x in (ObjectDerivation C) . { the Object of C} ; ::_thesis: x in the carrier' of C 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 Def3; 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 x in the carrier' of C ; ::_thesis: verum end; then reconsider A = (ObjectDerivation C) . { the Object of C} as Subset of the carrier' of C ; set O = (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}); (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) c= the carrier of C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) or x in the carrier of C ) assume x in (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) ; ::_thesis: x in the carrier of C 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 Def4; 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 x in the carrier of C ; ::_thesis: verum end; then reconsider O = (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) as Subset of the carrier of C ; set M9 = ConceptStr(# O,A #); ( the Object of C in { the Object of C} & t c= (AttributeDerivation C) . ((ObjectDerivation C) . t) ) by Th5, TARSKI:def_1; then reconsider M9 = ConceptStr(# O,A #) as non empty ConceptStr over C by Def8; (ObjectDerivation C) . the Extent of M9 = (ObjectDerivation C) . t by Th7 .= the Intent of M9 ; then M9 is concept-like by Def10; hence ex b1 being ConceptStr over C st ( b1 is concept-like & not b1 is empty ) ; ::_thesis: verum end; end; definition let C be FormalContext; mode FormalConcept of C is non empty concept-like ConceptStr over C; end; registration let C be FormalContext; cluster strict non empty concept-like for ConceptStr over C; existence ex b1 being FormalConcept of C st b1 is strict proof set CP = the FormalConcept of C; A1: ( (ObjectDerivation C) . the Extent of the FormalConcept of C = the Intent of the FormalConcept of C & (AttributeDerivation C) . the Intent of the FormalConcept of C = the Extent of the FormalConcept of C ) by Def10; ( not the Intent of the FormalConcept of C is empty or not the Extent of the FormalConcept of C is empty ) by Def8; then ConceptStr(# the Extent of the FormalConcept of C, the Intent of the FormalConcept of C #) is FormalConcept of C by A1, Def8, Def10; hence ex b1 being FormalConcept of C st b1 is strict ; ::_thesis: verum end; end; theorem Th19: :: CONLAT_1:19 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 for 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; ::_thesis: 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 for 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 ) ) let O be Subset of the carrier of C; ::_thesis: ( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C for 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 ) ) A1: for O9 being Subset of the carrier of C for 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; ::_thesis: for 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 let A9 be Subset of the carrier' of C; ::_thesis: ( ConceptStr(# O9,A9 #) is FormalConcept of C & O c= O9 implies (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 ) assume that A2: ConceptStr(# O9,A9 #) is FormalConcept of C and A3: O c= O9 ; ::_thesis: (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 reconsider M9 = ConceptStr(# O9,A9 #) as FormalConcept of C by A2; A4: (AttributeDerivation C) . A9 = the Extent of M9 by Def10 .= O9 ; A5: (ObjectDerivation C) . O9 = the Intent of M9 by Def10 .= A9 ; (ObjectDerivation C) . O9 c= (ObjectDerivation C) . O by A3, Th3; hence (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 by A4, A5, Th4; ::_thesis: verum 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 ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) = the Intent of ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) by Th7; hence ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C by Def10, Lm1; ::_thesis: verum end; hence ( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C for 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 ) ) by A1; ::_thesis: verum end; theorem :: CONLAT_1:20 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; ::_thesis: 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 ) let O be Subset of the carrier of C; ::_thesis: ( ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C iff (AttributeDerivation C) . ((ObjectDerivation C) . O) = O ) A1: now__::_thesis:_(_ex_A_being_Subset_of_the_carrier'_of_C_st_ConceptStr(#_O,A_#)_is_FormalConcept_of_C_implies_(AttributeDerivation_C)_._((ObjectDerivation_C)_._O)_=_O_) O c= (AttributeDerivation C) . ((ObjectDerivation C) . O) by Th5; then A2: for x being set st x in O holds 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 ; ::_thesis: (AttributeDerivation C) . ((ObjectDerivation C) . O) = O (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O by A3, Th19; then for x being set st x in (AttributeDerivation C) . ((ObjectDerivation C) . O) holds x in O ; hence (AttributeDerivation C) . ((ObjectDerivation C) . O) = O by A2, TARSKI:1; ::_thesis: verum end; now__::_thesis:_(_(AttributeDerivation_C)_._((ObjectDerivation_C)_._O)_=_O_implies_ex_A_being_Subset_of_the_carrier'_of_C_st_ConceptStr(#_O,A_#)_is_FormalConcept_of_C_) reconsider A = (ObjectDerivation C) . O as Subset of the carrier' of C ; set M9 = ConceptStr(# O,A #); assume (AttributeDerivation C) . ((ObjectDerivation C) . O) = O ; ::_thesis: ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C then ConceptStr(# O,A #) is FormalConcept of C by Def10, Lm1; hence ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C ; ::_thesis: verum end; hence ( ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C iff (AttributeDerivation C) . ((ObjectDerivation C) . O) = O ) by A1; ::_thesis: verum end; theorem Th21: :: CONLAT_1:21 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 for 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; ::_thesis: 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 for 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 ) ) let A be Subset of the carrier' of C; ::_thesis: ( ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C for 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 ) ) A1: for O9 being Subset of the carrier of C for 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; ::_thesis: for 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 let A9 be Subset of the carrier' of C; ::_thesis: ( ConceptStr(# O9,A9 #) is FormalConcept of C & A c= A9 implies (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 ) assume that A2: ConceptStr(# O9,A9 #) is FormalConcept of C and A3: A c= A9 ; ::_thesis: (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 reconsider M9 = ConceptStr(# O9,A9 #) as FormalConcept of C by A2; A4: (AttributeDerivation C) . A9 = the Extent of M9 by Def10 .= O9 ; A5: (ObjectDerivation C) . O9 = the Intent of M9 by Def10 .= A9 ; (AttributeDerivation C) . A9 c= (AttributeDerivation C) . A by A3, Th4; hence (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 by A4, A5, Th3; ::_thesis: verum 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 ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) = the Extent of ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) by Th8; hence ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C by Def10, Lm1; ::_thesis: verum end; hence ( ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C for 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 ) ) by A1; ::_thesis: verum end; theorem :: CONLAT_1:22 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; ::_thesis: 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 ) let A be Subset of the carrier' of C; ::_thesis: ( ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A ) A1: now__::_thesis:_(_ex_O_being_Subset_of_the_carrier_of_C_st_ConceptStr(#_O,A_#)_is_FormalConcept_of_C_implies_(ObjectDerivation_C)_._((AttributeDerivation_C)_._A)_=_A_) A c= (ObjectDerivation C) . ((AttributeDerivation C) . A) by Th6; then A2: for x being set st x in A holds 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 ; ::_thesis: (ObjectDerivation C) . ((AttributeDerivation C) . A) = A (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A by A3, Th21; then for x being set st x in (ObjectDerivation C) . ((AttributeDerivation C) . A) holds x in A ; hence (ObjectDerivation C) . ((AttributeDerivation C) . A) = A by A2, TARSKI:1; ::_thesis: verum end; now__::_thesis:_(_(ObjectDerivation_C)_._((AttributeDerivation_C)_._A)_=_A_implies_ex_O_being_Subset_of_the_carrier_of_C_st_ConceptStr(#_O,A_#)_is_FormalConcept_of_C_) reconsider O = (AttributeDerivation C) . A as Subset of the carrier of C ; set M9 = ConceptStr(# O,A #); assume (ObjectDerivation C) . ((AttributeDerivation C) . A) = A ; ::_thesis: ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C then ConceptStr(# O,A #) is FormalConcept of C by Def10, Lm1; hence ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C ; ::_thesis: verum end; hence ( ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A ) by A1; ::_thesis: verum end; definition let C be FormalContext; let CP be ConceptStr over C; attrCP is universal means :Def11: :: CONLAT_1:def 11 the Extent of CP = the carrier of C; end; :: deftheorem Def11 defines universal CONLAT_1:def_11_:_ for C being FormalContext for CP being ConceptStr over C holds ( CP is universal iff the Extent of CP = the carrier of C ); definition let C be FormalContext; let CP be ConceptStr over C; attrCP is co-universal means :Def12: :: CONLAT_1:def 12 the Intent of CP = the carrier' of C; end; :: deftheorem Def12 defines co-universal CONLAT_1:def_12_:_ for C being FormalContext for CP being ConceptStr over C holds ( CP is co-universal iff the Intent of CP = the carrier' of C ); registration let C be FormalContext; cluster strict non empty concept-like universal for ConceptStr over C; existence ex b1 being FormalConcept of C st ( b1 is strict & b1 is universal ) 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 by Def11; hence ex b1 being FormalConcept of C st ( b1 is strict & b1 is universal ) ; ::_thesis: verum end; cluster strict non empty concept-like co-universal for ConceptStr over C; existence ex b1 being FormalConcept of C st ( b1 is strict & b1 is co-universal ) 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 by Def12; hence ex b1 being FormalConcept of C st ( b1 is strict & b1 is co-universal ) ; ::_thesis: verum end; end; definition let C be FormalContext; func Concept-with-all-Objects C -> strict universal FormalConcept of C means :Def13: :: CONLAT_1:def 13 ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( it = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ); existence ex b1 being strict universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) 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 by Def11; hence ex b1 being strict universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict universal FormalConcept of C st ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) & ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) holds b1 = b2 ; end; :: deftheorem Def13 defines Concept-with-all-Objects CONLAT_1:def_13_:_ for C being FormalContext for b2 being strict universal FormalConcept of C holds ( b2 = Concept-with-all-Objects C iff ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) ); definition let C be FormalContext; func Concept-with-all-Attributes C -> strict co-universal FormalConcept of C means :Def14: :: CONLAT_1:def 14 ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( it = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ); existence ex b1 being strict co-universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) 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 by Def12; hence ex b1 being strict co-universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict co-universal FormalConcept of C st ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) & ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) holds b1 = b2 ; end; :: deftheorem Def14 defines Concept-with-all-Attributes CONLAT_1:def_14_:_ for C being FormalContext for b2 being strict co-universal FormalConcept of C holds ( b2 = Concept-with-all-Attributes C iff ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) ); theorem Th23: :: CONLAT_1:23 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; ::_thesis: ( the Extent of (Concept-with-all-Objects C) = the carrier of C & the Intent of (Concept-with-all-Attributes C) = the carrier' of C ) ( ex O being Subset of the carrier of C ex 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 ex 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 Def13, Def14; hence ( the Extent of (Concept-with-all-Objects C) = the carrier of C & the Intent of (Concept-with-all-Attributes C) = the carrier' of C ) by Th17, Th18; ::_thesis: verum end; theorem :: CONLAT_1:24 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; ::_thesis: for CP being FormalConcept of C holds ( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) ) let CP be FormalConcept of C; ::_thesis: ( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) ) A1: (AttributeDerivation C) . the Intent of CP = the Extent of CP by Def10; A2: now__::_thesis:_(_the_Intent_of_CP_=_{}_implies_CP_is_universal_) assume the Intent of CP = {} ; ::_thesis: CP is universal then the Extent of CP = the carrier of C by A1, Th18; hence CP is universal by Def11; ::_thesis: verum end; A3: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def10; now__::_thesis:_(_the_Extent_of_CP_=_{}_implies_CP_is_co-universal_) assume the Extent of CP = {} ; ::_thesis: CP is co-universal then the Intent of CP = the carrier' of C by A3, Th17; hence CP is co-universal by Def12; ::_thesis: verum end; hence ( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) ) by A2; ::_thesis: verum end; theorem Th25: :: CONLAT_1:25 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; ::_thesis: 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 ) ) let CP be strict FormalConcept of C; ::_thesis: ( ( the Extent of CP = {} implies CP = Concept-with-all-Attributes C ) & ( the Intent of CP = {} implies CP = Concept-with-all-Objects C ) ) A1: (AttributeDerivation C) . the Intent of CP = the Extent of CP by Def10; A2: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def10; A3: now__::_thesis:_(_the_Intent_of_CP_=_{}_implies_CP_=_Concept-with-all-Objects_C_) assume A4: the Intent of CP = {} ; ::_thesis: CP = Concept-with-all-Objects C then the Extent of CP = the carrier of C by A1, Th18; then CP is universal by Def11; hence CP = Concept-with-all-Objects C by A2, A1, A4, Def13; ::_thesis: verum end; now__::_thesis:_(_the_Extent_of_CP_=_{}_implies_CP_=_Concept-with-all-Attributes_C_) assume A5: the Extent of CP = {} ; ::_thesis: CP = Concept-with-all-Attributes C then the Intent of CP = the carrier' of C by A2, Th17; then CP is co-universal by Def12; hence CP = Concept-with-all-Attributes C by A2, A1, A5, Def14; ::_thesis: verum end; hence ( ( the Extent of CP = {} implies CP = Concept-with-all-Attributes C ) & ( the Intent of CP = {} implies CP = Concept-with-all-Objects C ) ) by A3; ::_thesis: verum end; theorem :: CONLAT_1:26 for C being FormalContext for CP being quasi-empty ConceptStr over C holds ( not CP is FormalConcept of C or CP is universal or CP is co-universal ) proof let C be FormalContext; ::_thesis: for CP being quasi-empty ConceptStr over C holds ( not CP is FormalConcept of C or CP is universal or CP is co-universal ) let CP be quasi-empty ConceptStr over C; ::_thesis: ( not CP is FormalConcept of C or CP is universal or CP is co-universal ) assume CP is FormalConcept of C ; ::_thesis: ( CP is universal or CP is co-universal ) then reconsider CP = CP as FormalConcept of C ; A1: (AttributeDerivation C) . the Intent of CP = the Extent of CP by Def10; A2: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def10; now__::_thesis:_(_(_the_Intent_of_CP_is_empty_&_CP_is_universal_)_or_(_the_Extent_of_CP_is_empty_&_CP_is_co-universal_)_) percases ( the Intent of CP is empty or the Extent of CP is empty ) by Def9; case the Intent of CP is empty ; ::_thesis: CP is universal then the Extent of CP = the carrier of C by A1, Th18; hence CP is universal by Def11; ::_thesis: verum end; case the Extent of CP is empty ; ::_thesis: CP is co-universal then the Intent of CP = the carrier' of C by A2, Th17; hence CP is co-universal by Def12; ::_thesis: verum end; end; end; hence ( CP is universal or CP is co-universal ) ; ::_thesis: verum end; theorem :: CONLAT_1:27 for C being FormalContext for CP being quasi-empty ConceptStr over C holds ( not CP is strict FormalConcept of C or CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C ) proof let C be FormalContext; ::_thesis: for CP being quasi-empty ConceptStr over C holds ( not CP is strict FormalConcept of C or CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C ) let CP be quasi-empty ConceptStr over C; ::_thesis: ( not CP is strict FormalConcept of C or CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C ) assume A1: CP is strict FormalConcept of C ; ::_thesis: ( CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C ) now__::_thesis:_(_(_the_Intent_of_CP_is_empty_&_CP_=_Concept-with-all-Objects_C_)_or_(_the_Extent_of_CP_is_empty_&_CP_=_Concept-with-all-Attributes_C_)_) percases ( the Intent of CP is empty or the Extent of CP is empty ) by Def9; case the Intent of CP is empty ; ::_thesis: CP = Concept-with-all-Objects C hence CP = Concept-with-all-Objects C by A1, Th25; ::_thesis: verum end; case the Extent of CP is empty ; ::_thesis: CP = Concept-with-all-Attributes C hence CP = Concept-with-all-Attributes C by A1, Th25; ::_thesis: verum end; end; end; hence ( CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C ) ; ::_thesis: verum end; definition let C be FormalContext; mode Set-of-FormalConcepts of C -> non empty set means :Def15: :: CONLAT_1:def 15 for X being set st X in it holds X is FormalConcept of C; existence ex b1 being non empty set st for X being set st X in b1 holds X is FormalConcept of C proof set CP = the FormalConcept of C; for X being set st X in { the FormalConcept of C} holds X is FormalConcept of C by TARSKI:def_1; hence ex b1 being non empty set st for X being set st X in b1 holds X is FormalConcept of C ; ::_thesis: verum end; end; :: deftheorem Def15 defines Set-of-FormalConcepts CONLAT_1:def_15_:_ for C being FormalContext for b2 being non empty set holds ( b2 is Set-of-FormalConcepts of C iff for X being set st X in b2 holds X is FormalConcept of C ); definition let C be FormalContext; let FCS be Set-of-FormalConcepts of C; :: original: Element redefine mode Element of FCS -> FormalConcept of C; coherence for b1 being Element of FCS holds b1 is FormalConcept of C by Def15; end; definition let C be FormalContext; let CP1, CP2 be FormalConcept of C; predCP1 is-SubConcept-of CP2 means :Def16: :: CONLAT_1:def 16 the Extent of CP1 c= the Extent of CP2; end; :: deftheorem Def16 defines is-SubConcept-of CONLAT_1:def_16_:_ for C being FormalContext for CP1, CP2 being FormalConcept of C holds ( CP1 is-SubConcept-of CP2 iff the Extent of CP1 c= the Extent of CP2 ); 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: :: CONLAT_1:28 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; ::_thesis: for CP1, CP2 being FormalConcept of C holds ( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 ) let CP1, CP2 be FormalConcept of C; ::_thesis: ( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 ) A1: now__::_thesis:_(_the_Intent_of_CP2_c=_the_Intent_of_CP1_implies_CP1_is-SubConcept-of_CP2_) assume the Intent of CP2 c= the Intent of CP1 ; ::_thesis: CP1 is-SubConcept-of CP2 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 Def10; hence CP1 is-SubConcept-of CP2 by A2, Def16; ::_thesis: verum end; now__::_thesis:_(_CP1_is-SubConcept-of_CP2_implies_the_Intent_of_CP2_c=_the_Intent_of_CP1_) assume CP1 is-SubConcept-of CP2 ; ::_thesis: the Intent of CP2 c= the Intent of CP1 then A3: the Extent of CP1 c= the Extent of CP2 by Def16; ( (ObjectDerivation C) . the Extent of CP2 = the Intent of CP2 & (ObjectDerivation C) . the Extent of CP1 = the Intent of CP1 ) by Def10; hence the Intent of CP2 c= the Intent of CP1 by A3, Th3; ::_thesis: verum end; hence ( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 ) by A1; ::_thesis: verum end; theorem :: CONLAT_1:29 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 :: CONLAT_1:30 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; ::_thesis: 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 ) let CP be FormalConcept of C; ::_thesis: ( CP is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Attributes C is-SubConcept-of CP ) 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 ( CP is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Attributes C is-SubConcept-of CP ) by A1, Def16, Th28; ::_thesis: verum end; begin definition let C be FormalContext; func B-carrier C -> non empty set equals :: CONLAT_1:def 17 { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } ; coherence { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } is non empty set proof set M9 = { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } ; not { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } is empty proof set CP = the FormalConcept of C; consider O being Subset of the carrier of C such that A1: O = the Extent of the FormalConcept of C ; consider A being Subset of the carrier' of C such that A2: A = the Intent of the FormalConcept of C ; A3: (AttributeDerivation C) . A = O by A1, A2, Def10; A4: (ObjectDerivation C) . O = A by A1, A2, Def10; then not ConceptStr(# O,A #) is empty by Lm1; then ConceptStr(# O,A #) in { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } by A4, A3; hence not { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } is empty ; ::_thesis: verum end; then reconsider M9 = { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } 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; ::_thesis: ( CP in M9 iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) ) now__::_thesis:_(_CP_in_M9_implies_(_(ObjectDerivation_C)_._the_Extent_of_CP_=_the_Intent_of_CP_&_(AttributeDerivation_C)_._the_Intent_of_CP_=_the_Extent_of_CP_)_) assume CP in M9 ; ::_thesis: ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st ( CP = ConceptStr(# E,I #) & not ConceptStr(# E,I #) is 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 ) ; ::_thesis: verum end; hence ( CP in M9 iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) ) ; ::_thesis: verum end; hence { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } is non empty set ; ::_thesis: verum end; end; :: deftheorem defines B-carrier CONLAT_1:def_17_:_ for C being FormalContext holds B-carrier C = { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } ; definition let C be FormalContext; :: original: B-carrier redefine func B-carrier C -> Set-of-FormalConcepts of C; coherence B-carrier C is Set-of-FormalConcepts of C proof for X being set st X in B-carrier C holds X is FormalConcept of C proof let X be set ; ::_thesis: ( X in B-carrier C implies X is FormalConcept of C ) assume X in B-carrier C ; ::_thesis: X is FormalConcept of C then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st ( X = ConceptStr(# E,I #) & not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) ; hence X is FormalConcept of C by Def10; ::_thesis: verum end; hence B-carrier C is Set-of-FormalConcepts of C by Def15; ::_thesis: verum end; end; registration let C be FormalContext; cluster B-carrier C -> non empty ; coherence not B-carrier C is empty ; end; theorem Th31: :: CONLAT_1:31 for C being FormalContext for CP being set holds ( CP in B-carrier C iff CP is strict FormalConcept of C ) proof let C be FormalContext; ::_thesis: for CP being set holds ( CP in B-carrier C iff CP is strict FormalConcept of C ) let CP be set ; ::_thesis: ( CP in B-carrier C iff CP is strict FormalConcept of C ) A1: ( CP is strict FormalConcept of C implies CP in B-carrier C ) proof assume A2: CP is strict FormalConcept of C ; ::_thesis: CP in B-carrier C then reconsider CP = CP as FormalConcept of C ; set I9 = the Intent of CP; set E9 = the Extent of CP; ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) by Def10; hence CP in B-carrier C by A2; ::_thesis: verum end; ( CP in B-carrier C implies CP is strict FormalConcept of C ) proof assume CP in B-carrier C ; ::_thesis: CP is strict FormalConcept of C then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st ( CP = ConceptStr(# E,I #) & not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) ; hence CP is strict FormalConcept of C by Def10; ::_thesis: verum end; hence ( CP in B-carrier C iff CP is strict FormalConcept of C ) by A1; ::_thesis: verum end; definition let C be FormalContext; func B-meet C -> BinOp of (B-carrier C) means :Def18: :: CONLAT_1:def 18 for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ex b1 being BinOp of (B-carrier C) st for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 . (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 defpred S1[ FormalConcept of C, FormalConcept of C, set ] means ex O being Subset of the carrier of C ex 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, CP2 being Element of B-carrier C ex CP being Element of B-carrier C st S1[CP1,CP2,CP] proof let CP1, CP2 be Element of B-carrier C; ::_thesis: ex CP being Element of B-carrier C st S1[CP1,CP2,CP] 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(# ( the Extent of CP1 /\ the Extent of CP2),((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) #); A2: (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) = (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 Def10 .= the Extent of CP1 /\ the Extent of CP2 by Def10 ; then A3: (ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2) = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) by Th7; then not ConceptStr(# ( the Extent of CP1 /\ the Extent of CP2),((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) #) is empty by Lm1; then ConceptStr(# ( the Extent of CP1 /\ the Extent of CP2),((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) #) in { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } by A2, A3; hence ex CP being Element of B-carrier C st S1[CP1,CP2,CP] ; ::_thesis: verum end; consider f being Function of [:(B-carrier C),(B-carrier C):],(B-carrier C) such that A4: for CP1, CP2 being Element of B-carrier C holds S1[CP1,CP2,f . (CP1,CP2)] from BINOP_1:sch_3(A1); reconsider f = f as BinOp of (B-carrier C) ; take f ; ::_thesis: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) ) for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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; ::_thesis: ex O being Subset of the carrier of C ex 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)) ) ( CP1 is Element of B-carrier C & CP2 is Element of B-carrier C ) by Th31; hence ex O being Subset of the carrier of C ex 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)) ) by A4; ::_thesis: verum end; hence for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) ) ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (B-carrier C) st ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 . (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)) ) ) & ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b2 . (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)) ) ) holds b1 = b2 proof let F1, F2 be BinOp of (B-carrier C); ::_thesis: ( ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) ) ) & ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) ) ) implies F1 = F2 ) assume A5: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) ) ; ::_thesis: ( ex CP1, CP2 being strict FormalConcept of C st for O being Subset of the carrier of C for A being Subset of the carrier' of C holds ( not F2 . (CP1,CP2) = ConceptStr(# O,A #) or not O = the Extent of CP1 /\ the Extent of CP2 or not A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) ) or F1 = F2 ) assume A6: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) ) ; ::_thesis: F1 = F2 A7: for X being set st X in [:(B-carrier C),(B-carrier C):] holds F1 . X = F2 . X proof let X be set ; ::_thesis: ( X in [:(B-carrier C),(B-carrier C):] implies F1 . X = F2 . X ) assume X in [:(B-carrier C),(B-carrier C):] ; ::_thesis: F1 . X = F2 . X then consider A, B being set 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 = B as strict FormalConcept of C by A9, Th31; reconsider A = A as strict FormalConcept of C by A8, Th31; ( ex O being Subset of the carrier of C ex 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 ex 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 F1 . X = F2 . X by A10; ::_thesis: verum end; ( dom F1 = [:(B-carrier C),(B-carrier C):] & dom F2 = [:(B-carrier C),(B-carrier C):] ) by FUNCT_2:def_1; hence F1 = F2 by A7, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def18 defines B-meet CONLAT_1:def_18_:_ for C being FormalContext for b2 being BinOp of (B-carrier C) holds ( b2 = B-meet C iff for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b2 . (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)) ) ); definition let C be FormalContext; func B-join C -> BinOp of (B-carrier C) means :Def19: :: CONLAT_1:def 19 for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ex b1 being BinOp of (B-carrier C) st for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 . (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 defpred S1[ FormalConcept of C, FormalConcept of C, set ] means ex O being Subset of the carrier of C ex 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, CP2 being Element of B-carrier C ex CP being Element of B-carrier C st S1[CP1,CP2,CP] proof let CP1, CP2 be Element of B-carrier C; ::_thesis: ex CP being Element of B-carrier C st S1[CP1,CP2,CP] 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(# ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),( the Intent of CP1 /\ the Intent of CP2) #); A2: (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))) = (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 Def10 .= the Intent of CP1 /\ the Intent of CP2 by Def10 ; then ( (AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2) = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & not ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),( the Intent of CP1 /\ the Intent of CP2) #) is empty ) by Lm1, Th7; then ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),( the Intent of CP1 /\ the Intent of CP2) #) in { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } by A2; hence ex CP being Element of B-carrier C st S1[CP1,CP2,CP] ; ::_thesis: verum end; consider f being Function of [:(B-carrier C),(B-carrier C):],(B-carrier C) such that A3: for CP1, CP2 being Element of B-carrier C holds S1[CP1,CP2,f . (CP1,CP2)] from BINOP_1:sch_3(A1); reconsider f = f as BinOp of (B-carrier C) ; take f ; ::_thesis: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ) for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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; ::_thesis: ex O being Subset of the carrier of C ex 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 ) ( CP1 is Element of B-carrier C & CP2 is Element of B-carrier C ) by Th31; hence ex O being Subset of the carrier of C ex 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 ) by A3; ::_thesis: verum end; hence for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ) ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (B-carrier C) st ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b1 . (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 ) ) & ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b2 . (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 ) ) holds b1 = b2 proof let F1, F2 be BinOp of (B-carrier C); ::_thesis: ( ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ) ) & ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ) ) implies F1 = F2 ) assume A4: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ) ; ::_thesis: ( ex CP1, CP2 being strict FormalConcept of C st for O being Subset of the carrier of C for A being Subset of the carrier' of C holds ( not F2 . (CP1,CP2) = ConceptStr(# O,A #) or not O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) or not A = the Intent of CP1 /\ the Intent of CP2 ) or F1 = F2 ) assume A5: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ) ; ::_thesis: F1 = F2 A6: for X being set st X in [:(B-carrier C),(B-carrier C):] holds F1 . X = F2 . X proof let X be set ; ::_thesis: ( X in [:(B-carrier C),(B-carrier C):] implies F1 . X = F2 . X ) assume X in [:(B-carrier C),(B-carrier C):] ; ::_thesis: F1 . X = F2 . X then consider A, B being set 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 = B as strict FormalConcept of C by A8, Th31; reconsider A = A as strict FormalConcept of C by A7, Th31; ( ex O being Subset of the carrier of C ex 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 ex 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 F1 . X = F2 . X by A9; ::_thesis: verum end; ( dom F1 = [:(B-carrier C),(B-carrier C):] & dom F2 = [:(B-carrier C),(B-carrier C):] ) by FUNCT_2:def_1; hence F1 = F2 by A6, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def19 defines B-join CONLAT_1:def_19_:_ for C being FormalContext for b2 being BinOp of (B-carrier C) holds ( b2 = B-join C iff for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st ( b2 . (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 ) ); 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; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,CP2) in rng (B-meet C) let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP1,CP2) in rng (B-meet 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 (B-meet C) . (CP1,CP2) in rng (B-meet C) by FUNCT_1:def_3; ::_thesis: verum 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; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) in rng (B-join C) let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-join C) . (CP1,CP2) in rng (B-join 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 (B-join C) . (CP1,CP2) in rng (B-join C) by FUNCT_1:def_3; ::_thesis: verum end; theorem Th32: :: CONLAT_1:32 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; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,CP2) = (B-meet C) . (CP2,CP1) let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP1,CP2) = (B-meet C) . (CP2,CP1) ( ex O being Subset of the carrier of C ex 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 ex 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 Def18; hence (B-meet C) . (CP1,CP2) = (B-meet C) . (CP2,CP1) ; ::_thesis: verum end; theorem Th33: :: CONLAT_1:33 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; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1) let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1) ( ex O being Subset of the carrier of C ex 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 ex 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 Def19; hence (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1) ; ::_thesis: verum end; theorem Th34: :: CONLAT_1:34 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; ::_thesis: 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) let CP1, CP2, CP3 be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP1,((B-meet C) . (CP2,CP3))) = (B-meet C) . (((B-meet C) . (CP1,CP2)),CP3) (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 ex 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 ex 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 Def18; (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 ex 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 ex 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 Def18; (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 (B-meet C) . (CP1,((B-meet C) . (CP2,CP3))) = (B-meet C) . (((B-meet C) . (CP1,CP2)),CP3) by A1, A2, XBOOLE_1:16; ::_thesis: verum end; theorem Th35: :: CONLAT_1:35 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; ::_thesis: 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) let CP1, CP2, CP3 be strict FormalConcept of C; ::_thesis: (B-join C) . (CP1,((B-join C) . (CP2,CP3))) = (B-join C) . (((B-join C) . (CP1,CP2)),CP3) (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 ex 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 ex 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 Def19; (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 ex 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 ex 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 Def19; (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 (B-join C) . (CP1,((B-join C) . (CP2,CP3))) = (B-join C) . (((B-join C) . (CP1,CP2)),CP3) by A1, A2, XBOOLE_1:16; ::_thesis: verum end; theorem Th36: :: CONLAT_1:36 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; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2 let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2 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 ex 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 ex 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 Def18, Def19; (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 Def10 .= the Extent of CP2 by Def10 ; ((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 Def10 .= ((ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2)) /\ the Intent of CP2 by Def10 .= ((ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP2) by Def10 .= (ObjectDerivation C) . the Extent of CP2 by A1, Th3, XBOOLE_1:28 .= the Intent of CP2 by Def10 ; hence (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2 by A2, A3; ::_thesis: verum end; theorem Th37: :: CONLAT_1:37 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; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,((B-join C) . (CP1,CP2))) = CP1 let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP1,((B-join C) . (CP1,CP2))) = CP1 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 ex 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 ex 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 Def18, Def19; (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 Def10 .= the Intent of CP1 by Def10 ; 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 Def10 .= the Extent of CP1 /\ ((AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2)) by Def10 .= ((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2)) by Def10 .= (AttributeDerivation C) . the Intent of CP1 by A1, Th4, XBOOLE_1:28 .= the Extent of CP1 by Def10 ; hence (B-meet C) . (CP1,((B-join C) . (CP1,CP2))) = CP1 by A2, A3; ::_thesis: verum end; theorem :: CONLAT_1:38 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; ::_thesis: for CP being strict FormalConcept of C holds (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP let CP be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP 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 Def18; 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, Def10 .= (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, Def10 .= (ObjectDerivation C) . the Extent of CP by Th7 .= the Intent of CP by Def10 ; hence (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP by A1, A4; ::_thesis: verum end; theorem Th39: :: CONLAT_1:39 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; ::_thesis: for CP being strict FormalConcept of C holds (B-join C) . (CP,(Concept-with-all-Objects C)) = Concept-with-all-Objects C let CP be strict FormalConcept of C; ::_thesis: (B-join C) . (CP,(Concept-with-all-Objects C)) = Concept-with-all-Objects 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 Def19; 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 Def10 .= the Extent of (Concept-with-all-Objects C) by Def10 ; A = ((ObjectDerivation C) . the Extent of CP) /\ the Intent of (Concept-with-all-Objects C) by A3, Def10 .= ((ObjectDerivation C) . the Extent of CP) /\ ((ObjectDerivation C) . the Extent of (Concept-with-all-Objects C)) by Def10 .= (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 Def10 ; hence (B-join C) . (CP,(Concept-with-all-Objects C)) = Concept-with-all-Objects C by A1, A4; ::_thesis: verum end; theorem :: CONLAT_1:40 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; ::_thesis: for CP being strict FormalConcept of C holds (B-join C) . (CP,(Concept-with-all-Attributes C)) = CP let CP be strict FormalConcept of C; ::_thesis: (B-join C) . (CP,(Concept-with-all-Attributes C)) = CP 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 Def19; 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, Def10 .= (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, Def10 .= (AttributeDerivation C) . the Intent of CP by Th8 .= the Extent of CP by Def10 ; hence (B-join C) . (CP,(Concept-with-all-Attributes C)) = CP by A1, A4; ::_thesis: verum end; theorem :: CONLAT_1:41 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; ::_thesis: for CP being strict FormalConcept of C holds (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C let CP be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes 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 Def18; 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 Def10 .= the Intent of (Concept-with-all-Attributes C) by Def10 ; O = ((AttributeDerivation C) . the Intent of CP) /\ the Extent of (Concept-with-all-Attributes C) by A2, Def10 .= ((AttributeDerivation C) . the Intent of CP) /\ ((AttributeDerivation C) . the Intent of (Concept-with-all-Attributes C)) by Def10 .= (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 Def10 ; hence (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C by A1, A4; ::_thesis: verum end; definition let C be FormalContext; func ConceptLattice C -> non empty strict LattStr equals :: CONLAT_1:def 20 LattStr(# (B-carrier C),(B-join C),(B-meet C) #); coherence LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr ; end; :: deftheorem defines ConceptLattice CONLAT_1:def_20_:_ for C being FormalContext holds ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #); theorem Th42: :: CONLAT_1:42 for C being FormalContext holds ConceptLattice C is Lattice proof let C be FormalContext; ::_thesis: ConceptLattice C is Lattice set L = LattStr(# (B-carrier C),(B-join C),(B-meet C) #); reconsider L = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) as non empty strict 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; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c reconsider b = b, c = c as Element of B-carrier C ; reconsider d = (B-join C) . (b,c) as Element of L ; reconsider b = b, c = c as Element of L ; reconsider a = a, b = b as Element of B-carrier C ; reconsider e = (B-join C) . (a,b) as Element of L ; reconsider a = a, b = 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 = a, b = b, c = 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 a "\/" (b "\/" c) = (a "\/" b) "\/" c by A2, A3; ::_thesis: verum end; A4: for a, b being Element of L holds (a "/\" b) "\/" b = b proof let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b reconsider a = a, b = b as Element of B-carrier C ; reconsider d = (B-meet C) . (a,b) as Element of L ; reconsider a = a, b = 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 = a, b = b as strict FormalConcept of C by Th31; (B-join C) . (((B-meet C) . (a,b)),b) = b by Th36; hence (a "/\" b) "\/" b = b by A5; ::_thesis: verum 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; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c reconsider b = b, c = c as Element of B-carrier C ; reconsider d = (B-meet C) . (b,c) as Element of L ; reconsider b = b, c = 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 = a, b = b as Element of B-carrier C ; reconsider e = (B-meet C) . (a,b) as Element of L ; reconsider a = a, b = 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 = a, b = b, c = 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 a "/\" (b "/\" c) = (a "/\" b) "/\" c by A7, A8; ::_thesis: verum end; A9: for a, b being Element of L holds a "/\" b = b "/\" a proof let a, b be Element of L; ::_thesis: a "/\" b = b "/\" a A10: b "/\" a = (B-meet C) . (b,a) by LATTICES:def_2; reconsider a = a, b = b as strict FormalConcept of C by Th31; (B-meet C) . (a,b) = (B-meet C) . (b,a) by Th32; hence a "/\" b = b "/\" a by A10, LATTICES:def_2; ::_thesis: verum end; A11: for a, b being Element of L holds a "/\" (a "\/" b) = a proof let a, b be Element of L; ::_thesis: a "/\" (a "\/" b) = a reconsider a = a, b = b as Element of B-carrier C ; reconsider d = (B-join C) . (a,b) as Element of L ; reconsider a = a, b = 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 = a, b = b as strict FormalConcept of C by Th31; (B-meet C) . (a,((B-join C) . (a,b))) = a by Th37; hence a "/\" (a "\/" b) = a by A12; ::_thesis: verum end; for a, b being Element of L holds a "\/" b = b "\/" a proof let a, b be Element of L; ::_thesis: a "\/" b = b "\/" a A13: b "\/" a = (B-join C) . (b,a) by LATTICES:def_1; reconsider a = a, b = b as strict FormalConcept of C by Th31; (B-join C) . (a,b) = (B-join C) . (b,a) by Th33; hence a "\/" b = b "\/" a by A13, LATTICES:def_1; ::_thesis: verum end; then ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by A1, A4, A9, A6, A11, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; hence ConceptLattice C is Lattice ; ::_thesis: verum end; registration let C be FormalContext; cluster ConceptLattice C -> non empty strict Lattice-like ; coherence ( ConceptLattice C is strict & not ConceptLattice C is empty & ConceptLattice C is Lattice-like ) by Th42; end; definition let C be FormalContext; let S be non empty Subset of (ConceptLattice C); :: original: Element redefine mode Element of S -> FormalConcept of C; coherence for b1 being Element of S holds b1 is FormalConcept of C proof let s be Element of S; ::_thesis: s is FormalConcept of C s is Element of B-carrier C ; hence s is FormalConcept of C ; ::_thesis: verum end; end; definition let C be FormalContext; let CP be Element of (ConceptLattice C); funcCP @ -> strict FormalConcept of C equals :: CONLAT_1:def 21 CP; coherence CP is strict FormalConcept of C by Th31; end; :: deftheorem defines @ CONLAT_1:def_21_:_ for C being FormalContext for CP being Element of (ConceptLattice C) holds CP @ = CP; theorem Th43: :: CONLAT_1:43 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; ::_thesis: for CP1, CP2 being Element of (ConceptLattice C) holds ( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ ) let CP1, CP2 be Element of (ConceptLattice C); ::_thesis: ( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ ) set CL = ConceptLattice C; A1: now__::_thesis:_(_CP1_@_is-SubConcept-of_CP2_@_implies_CP1_[=_CP2_) assume A2: CP1 @ is-SubConcept-of CP2 @ ; ::_thesis: CP1 [= 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 Def19; the Extent of (CP1 @) c= the Extent of (CP2 @) by A2, Def16; 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, Def10 .= the Extent of (CP2 @) by Def10 ; then CP1 "\/" CP2 = CP2 by A3, A4, A6, LATTICES:def_1; hence CP1 [= CP2 by LATTICES:def_3; ::_thesis: verum end; now__::_thesis:_(_CP1_[=_CP2_implies_CP1_@_is-SubConcept-of_CP2_@_) assume CP1 [= CP2 ; ::_thesis: CP1 @ is-SubConcept-of CP2 @ then CP1 "\/" CP2 = CP2 by LATTICES:def_3; then A7: the L_join of (ConceptLattice C) . (CP1,CP2) = CP2 by LATTICES:def_1; ex O being Subset of the carrier of C ex 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 Def19; then for x being set st x in the Intent of (CP2 @) holds x in the Intent of (CP1 @) by A7, XBOOLE_0:def_4; then the Intent of (CP2 @) c= the Intent of (CP1 @) by TARSKI:def_3; hence CP1 @ is-SubConcept-of CP2 @ by Th28; ::_thesis: verum end; hence ( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ ) by A1; ::_thesis: verum end; theorem Th44: :: CONLAT_1:44 for C being FormalContext holds ConceptLattice C is complete Lattice proof let C be FormalContext; ::_thesis: ConceptLattice C is complete Lattice 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); ::_thesis: 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 ) ) percases ( X = {} or X <> {} ) ; supposeA1: X = {} ; ::_thesis: 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 ) ) 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); ::_thesis: ( b is_less_than X implies b [= Top (ConceptLattice C) ) assume b is_less_than X ; ::_thesis: b [= Top (ConceptLattice C) 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); ::_thesis: ( CO "\/" CP = CO & CP "\/" CO = CO ) reconsider CP = CP as strict FormalConcept of C by Th31; reconsider CO = CO as strict FormalConcept of C ; (B-join C) . (CO,CP) = (B-join C) . (CP,CO) by Th33 .= CO by Th39 ; hence ( CO "\/" CP = CO & CP "\/" CO = CO ) by LATTICES:def_1; ::_thesis: verum end; hence ex c being Element of (ConceptLattice C) st for a being Element of (ConceptLattice C) holds ( c "\/" a = c & a "\/" c = c ) ; ::_thesis: verum end; then ConceptLattice C is upper-bounded by LATTICES:def_14; then (Top (ConceptLattice C)) "\/" b = Top (ConceptLattice C) ; hence b [= Top (ConceptLattice C) by LATTICES:def_3; ::_thesis: verum 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 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 ) ) by A2; ::_thesis: verum end; suppose X <> {} ; ::_thesis: 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 ) ) then reconsider X = 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 { the Extent of x where x is Element of B-carrier C : x in X } proof let x be Element of X; ::_thesis: the Extent of x in { the Extent of x where x is Element of B-carrier C : x in X } x in X ; then reconsider x = x as Element of B-carrier C ; the Extent of x in { the Extent of x where x is Element of B-carrier C : x in X } ; hence the Extent of x in { the Extent of x where x is Element of B-carrier C : x in X } ; ::_thesis: verum end; then reconsider ExX = { the Extent of x where x is Element of B-carrier C : x in X } as non empty set ; set E1 = meet ExX; A4: for o being Object of C holds ( o in meet ExX iff for x being Element of X holds o in the Extent of x ) proof let o be Object of C; ::_thesis: ( o in meet ExX iff for x being Element of X holds o in the Extent of x ) A5: ( ( for x being Element of X holds o in the Extent of x ) implies o in meet ExX ) proof assume A6: for x being Element of X holds o in the Extent of x ; ::_thesis: o in meet ExX for Y being set st Y in ExX holds o in Y proof let Y be set ; ::_thesis: ( Y in ExX implies o in Y ) assume Y in ExX ; ::_thesis: o in Y then ex Y9 being Element of B-carrier C st ( Y = the Extent of Y9 & Y9 in X ) ; hence o in Y by A6; ::_thesis: verum end; hence o in meet ExX by SETFAM_1:def_1; ::_thesis: verum end; ( o in meet ExX implies for x being Element of X holds o in the Extent of x ) proof assume A7: o in meet ExX ; ::_thesis: for x being Element of X holds o in the Extent of x let x be Element of X; ::_thesis: o in the Extent of x the Extent of x in ExX by A3; hence o in the Extent of x by A7, SETFAM_1:def_1; ::_thesis: verum end; hence ( o in meet ExX iff for x being Element of X holds o in the Extent of x ) by A5; ::_thesis: verum end; meet ExX c= the carrier of C proof set Y = the Element of ExX; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet ExX or x in the carrier of C ) the Element of ExX in ExX ; then consider Y9 being Element of B-carrier C such that A8: the Element of ExX = the Extent of Y9 and Y9 in X ; assume x in meet ExX ; ::_thesis: x in the carrier of C then x in the Extent of Y9 by A8, SETFAM_1:def_1; hence x in the carrier of C ; ::_thesis: verum 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 { the Intent of x where x is Element of B-carrier C : x in X } ; A10: for a being Attribute of C holds ( a in union { the Intent of x where x is Element of B-carrier C : x in X } iff ex x being Element of X st a in the Intent of x ) proof let a be Attribute of C; ::_thesis: ( a in union { the Intent of x where x is Element of B-carrier C : x in X } iff ex x being Element of X st a in the Intent of x ) A11: ( ex x being Element of X st a in the Intent of x implies a in union { the Intent of x where x is Element of B-carrier C : x in X } ) proof assume A12: ex x being Element of X st a in the Intent of x ; ::_thesis: a in union { the Intent of x where x is Element of B-carrier C : x in X } ex Y being set st ( a in Y & Y in { the Intent of x where x is Element of B-carrier C : x in X } ) 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 { the Intent of x where x is Element of B-carrier C : x in X } ; hence ex Y being set st ( a in Y & Y in { the Intent of x where x is Element of B-carrier C : x in X } ) by A13; ::_thesis: verum end; hence a in union { the Intent of x where x is Element of B-carrier C : x in X } by TARSKI:def_4; ::_thesis: verum end; ( a in union { the Intent of x where x is Element of B-carrier C : x in X } implies ex x being Element of X st a in the Intent of x ) proof assume a in union { the Intent of x where x is Element of B-carrier C : x in X } ; ::_thesis: ex x being Element of X st a in the Intent of x then consider Y being set such that A14: a in Y and A15: Y in { the Intent of x where x is Element of B-carrier C : x in X } by TARSKI:def_4; ex Y9 being Element of B-carrier C st ( Y = the Intent of Y9 & Y9 in X ) by A15; hence ex x being Element of X st a in the Intent of x by A14; ::_thesis: verum end; hence ( a in union { the Intent of x where x is Element of B-carrier C : x in X } iff ex x being Element of X st a in the Intent of x ) by A11; ::_thesis: verum end; union { the Intent of x where x is Element of B-carrier C : x in X } c= the carrier' of C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { the Intent of x where x is Element of B-carrier C : x in X } or x in the carrier' of C ) assume x in union { the Intent of x where x is Element of B-carrier C : x in X } ; ::_thesis: x in the carrier' of C then consider Y being set such that A16: x in Y and A17: Y in { the Intent of x where x is Element of B-carrier C : x in X } by TARSKI:def_4; ex Y9 being Element of B-carrier C st ( Y = the Intent of Y9 & Y9 in X ) by A17; hence x in the carrier' of C by A16; ::_thesis: verum 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; ::_thesis: ( o in O iff for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ) 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 ; ::_thesis: o in O for x being Element of X holds o in the Extent of x proof let x be Element of X; ::_thesis: o in the Extent of x o in (AttributeDerivation C) . the Intent of x by A21; hence o in the Extent of x by Def10; ::_thesis: verum end; hence o in O by A9; ::_thesis: verum 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 ; ::_thesis: for x being Element of X holds o in (AttributeDerivation C) . the Intent of x for x being Element of X holds o in (AttributeDerivation C) . the Intent of x proof let x be Element of X; ::_thesis: o in (AttributeDerivation C) . the Intent of x o in the Extent of x by A9, A22; hence o in (AttributeDerivation C) . the Intent of x by Def10; ::_thesis: verum end; hence for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ; ::_thesis: verum end; hence ( o in O iff for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ) by A20; ::_thesis: verum end; A23: for x being set st x in (AttributeDerivation C) . A9 holds x in O proof let x be set ; ::_thesis: ( x in (AttributeDerivation C) . A9 implies x in O ) assume x in (AttributeDerivation C) . A9 ; ::_thesis: x in O 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 Def4; 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; ::_thesis: x9 in (AttributeDerivation C) . the Intent of x for a being Attribute of C st a in the Intent of x holds x9 is-connected-with a proof let a be Attribute of C; ::_thesis: ( a in the Intent of x implies x9 is-connected-with a ) assume a in the Intent of x ; ::_thesis: x9 is-connected-with a then a in A9 by A18; hence x9 is-connected-with a by A25; ::_thesis: verum end; 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 x9 in (AttributeDerivation C) . the Intent of x by Def4; ::_thesis: verum end; hence x in O by A19, A24; ::_thesis: verum 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 set st x in O holds x in (AttributeDerivation C) . A9 proof let x9 be set ; ::_thesis: ( x9 in O implies x9 in (AttributeDerivation C) . A9 ) assume A27: x9 in O ; ::_thesis: x9 in (AttributeDerivation C) . A9 then reconsider x9 = 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; ::_thesis: ( a in A9 implies x9 is-connected-with a ) assume a in A9 ; ::_thesis: x9 is-connected-with a 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 Def4; 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 x9 is-connected-with a by A28; ::_thesis: verum 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 x9 in (AttributeDerivation C) . A9 by Def4; ::_thesis: verum end; then O = (AttributeDerivation C) . A9 by A23, TARSKI:1; then ConceptStr(# O,A #) is FormalConcept of C by A26, Th21; then reconsider p = ConceptStr(# O,A #) 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); ::_thesis: ( b is_less_than X implies b [= p ) assume A30: b is_less_than X ; ::_thesis: b [= p the Extent of (b @) c= the Extent of (p @) proof let x9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x9 in the Extent of (b @) or x9 in the Extent of (p @) ) assume A31: x9 in the Extent of (b @) ; ::_thesis: x9 in the Extent of (p @) then reconsider x9 = 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; ::_thesis: x9 in the Extent of x x in X ; then reconsider x = 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 @) by Def16; hence x9 in the Extent of x by A31; ::_thesis: verum end; hence x9 in the Extent of (p @) by A9; ::_thesis: verum end; then b @ is-SubConcept-of p @ by Def16; hence b [= p by Th43; ::_thesis: verum end; for q being Element of (ConceptLattice C) st q in X holds p [= q proof let q be Element of (ConceptLattice C); ::_thesis: ( q in X implies p [= q ) assume A32: q in X ; ::_thesis: p [= q the Extent of (p @) c= the Extent of (q @) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Extent of (p @) or x in the Extent of (q @) ) assume x in the Extent of (p @) ; ::_thesis: x in the Extent of (q @) hence x in the Extent of (q @) by A9, A32; ::_thesis: verum end; then p @ is-SubConcept-of q @ by Def16; hence p [= q by Th43; ::_thesis: verum end; then p is_less_than X by LATTICE3:def_16; hence 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 ) ) by A29; ::_thesis: verum end; end; end; hence ConceptLattice C is complete Lattice by VECTSP_8:def_6; ::_thesis: verum end; registration let C be FormalContext; cluster ConceptLattice C -> non empty strict complete ; coherence ConceptLattice C is complete by Th44; end;