conlat_1.miz



    begin

    registration

      cluster strict non empty non void for 2-sorted;

      existence

      proof

         2-sorted (# { {} }, { {} } #) is non empty non void;

        hence thesis;

      end;

    end

    definition

      ::$Canceled

      struct ( 2-sorted) ContextStr (# the carrier, carrier' -> set,

the Information -> Relation of the carrier, the carrier' #)

       attr strict strict;

    end

    registration

      cluster strict non empty non void for ContextStr;

      existence

      proof

         ContextStr (# { {} }, { {} }, the Relation of { {} }, { {} } #) is non empty non void;

        hence thesis;

      end;

    end

    definition

      mode FormalContext is non empty non void ContextStr;

    end

    definition

      let C be 2-sorted;

      mode Object of C is Element of C;

      mode Attribute of C is Element of the carrier' of C;

    end

    registration

      let C be non empty non void 2-sorted;

      cluster the carrier' of C -> non empty;

      coherence ;

      cluster the carrier of C -> non empty;

      coherence ;

    end

    registration

      let C be non empty non void 2-sorted;

      cluster non empty for Subset of the carrier of C;

      existence

      proof

        take the carrier of C;

        the carrier of C c= the carrier of C;

        hence thesis;

      end;

      cluster non empty for Subset of the carrier' of C;

      existence

      proof

        take the carrier' of C;

        the carrier' of C c= the carrier' of C;

        hence thesis;

      end;

    end

    definition

      let C be FormalContext;

      let o be Object of C;

      let a be Attribute of C;

      :: CONLAT_1:def2

      pred o is-connected-with a means [o, a] in the Information of C;

    end

    notation

      let C be FormalContext;

      let o be Object of C;

      let a be Attribute of C;

      antonym o is-not-connected-with a for o is-connected-with a;

    end

    begin

    definition

      let C be FormalContext;

      :: CONLAT_1:def3

      func ObjectDerivation (C) -> Function of ( bool the carrier of C), ( bool the carrier' of C) means

      : Def2: for O be Subset of the carrier of C holds (it . O) = { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a };

      existence

      proof

        set f = the set of all [O, { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a }] where O be Subset of the carrier of C;

        for u be object st u in f holds ex v,w be object st u = [v, w]

        proof

          let u be object;

          assume u in f;

          then ex O be Subset of the carrier of C st u = [O, { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a }];

          hence thesis;

        end;

        then

        reconsider f as Relation by RELAT_1:def 1;

        for u,v1,v2 be object st [u, v1] in f & [u, v2] in f holds v1 = v2

        proof

          let u,v1,v2 be object;

          assume that

           A1: [u, v1] in f and

           A2: [u, v2] in f;

          consider O be Subset of the carrier of C such that

           A3: [u, v1] = [O, { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a }] by A1;

          

           A4: v1 = ( [u, v1] `2 )

          .= ( [O, { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a }] `2 ) by A3

          .= { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a };

          consider O9 be Subset of the carrier of C such that

           A5: [u, v2] = [O9, { a where a be Attribute of C : for o be Object of C st o in O9 holds o is-connected-with a }] by A2;

          

           A6: v2 = ( [u, v2] `2 )

          .= ( [O9, { a where a be Attribute of C : for o be Object of C st o in O9 holds o is-connected-with a }] `2 ) by A5

          .= { a where a be Attribute of C : for o be Object of C st o in O9 holds o is-connected-with a };

          O = ( [O, { a where a be Attribute of C : for o be 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 be Attribute of C : for o be Object of C st o in O9 holds o is-connected-with a }] `1 ) by A5

          .= O9;

          hence thesis by A4, A6;

        end;

        then

        reconsider f as Function by FUNCT_1:def 1;

        

         A7: for x be object holds x in ( dom f) implies x in ( bool the carrier of C)

        proof

          let x be object;

          assume x in ( dom f);

          then

          consider y be object such that

           A8: [x, y] in f by XTUPLE_0:def 12;

          consider O be Subset of the carrier of C such that

           A9: [x, y] = [O, { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a }] by A8;

          x = ( [x, y] `1 )

          .= ( [O, { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a }] `1 ) by A9

          .= O;

          hence thesis;

        end;

        for x be object holds x in ( bool the carrier of C) implies x in ( dom f)

        proof

          let x be object;

          assume x in ( bool the carrier of C);

          then

          reconsider x as Subset of the carrier of C;

           [x, { a where a be Attribute of C : for o be Object of C st o in x holds o is-connected-with a }] in f;

          hence thesis by XTUPLE_0:def 12;

        end;

        then

         A10: ( dom f) = ( bool the carrier of C) by A7, TARSKI: 2;

        ( rng f) c= ( bool the carrier' of C)

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A11: [x, y] in f by XTUPLE_0:def 13;

          consider O be Subset of the carrier of C such that

           A12: [x, y] = [O, { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a }] by A11;

          

           A13: { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a } c= the carrier' of C

          proof

            let u be object;

            assume u in { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a };

            then ex u9 be Attribute of C st u9 = u & for o be Object of C st o in O holds o is-connected-with u9;

            hence thesis;

          end;

          y = ( [x, y] `2 )

          .= ( [O, { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a }] `2 ) by A12

          .= { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a };

          hence thesis by A13;

        end;

        then

        reconsider f as Function of ( bool the carrier of C), ( bool the carrier' of C) by A10, FUNCT_2:def 1, RELSET_1: 4;

        take f;

        for O be Subset of the carrier of C holds (f . O) = { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a }

        proof

          let O be Subset of the carrier of C;

          consider y be object such that

           A14: [O, y] in f by A10, XTUPLE_0:def 12;

          consider O9 be Subset of the carrier of C such that

           A15: [O, y] = [O9, { a where a be Attribute of C : for o be Object of C st o in O9 holds o is-connected-with a }] by A14;

          

           A16: y = ( [O, y] `2 )

          .= ( [O9, { a where a be Attribute of C : for o be Object of C st o in O9 holds o is-connected-with a }] `2 ) by A15

          .= { a where a be Attribute of C : for o be Object of C st o in O9 holds o is-connected-with a };

          O = ( [O, y] `1 )

          .= ( [O9, { a where a be Attribute of C : for o be Object of C st o in O9 holds o is-connected-with a }] `1 ) by A15

          .= O9;

          hence thesis by A10, A14, A16, FUNCT_1:def 2;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( bool the carrier of C), ( bool the carrier' of C);

        assume

         A17: for O be Subset of the carrier of C holds (F1 . O) = { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a };

        assume

         A18: for O be Subset of the carrier of C holds (F2 . O) = { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a };

        

         A19: for O be object st O in ( bool the carrier of C) holds (F1 . O) = (F2 . O)

        proof

          let O be object;

          assume O in ( bool the carrier of C);

          then

          reconsider O as Subset of the carrier of C;

          (F1 . O) = { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a } by A17

          .= (F2 . O) by A18;

          hence thesis;

        end;

        ( dom F1) = ( bool the carrier of C) & ( dom F2) = ( bool the carrier of C) by FUNCT_2:def 1;

        hence thesis by A19, FUNCT_1: 2;

      end;

    end

    definition

      let C be FormalContext;

      :: CONLAT_1:def4

      func AttributeDerivation (C) -> Function of ( bool the carrier' of C), ( bool the carrier of C) means

      : Def3: for A be Subset of the carrier' of C holds (it . A) = { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a };

      existence

      proof

        set f = the set of all [A, { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a }] where A be Subset of the carrier' of C;

        for u be object st u in f holds ex v,w be object st u = [v, w]

        proof

          let u be object;

          assume u in f;

          then ex A be Subset of the carrier' of C st u = [A, { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a }];

          hence thesis;

        end;

        then

        reconsider f as Relation by RELAT_1:def 1;

        for u,v1,v2 be object st [u, v1] in f & [u, v2] in f holds v1 = v2

        proof

          let u,v1,v2 be object;

          assume that

           A1: [u, v1] in f and

           A2: [u, v2] in f;

          consider A be Subset of the carrier' of C such that

           A3: [u, v1] = [A, { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a }] by A1;

          

           A4: v1 = ( [u, v1] `2 )

          .= ( [A, { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a }] `2 ) by A3

          .= { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a };

          consider A9 be Subset of the carrier' of C such that

           A5: [u, v2] = [A9, { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a }] by A2;

          

           A6: v2 = ( [u, v2] `2 )

          .= ( [A9, { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a }] `2 ) by A5

          .= ( [A9, { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a }] `2 )

          .= { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a };

          A = ( [A, { o where o be Object of C : for a be 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 be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a }] `1 ) by A5

          .= A9;

          hence thesis by A4, A6;

        end;

        then

        reconsider f as Function by FUNCT_1:def 1;

        

         A7: for x be object holds x in ( dom f) implies x in ( bool the carrier' of C)

        proof

          let x be object;

          assume x in ( dom f);

          then

          consider y be object such that

           A8: [x, y] in f by XTUPLE_0:def 12;

          consider A be Subset of the carrier' of C such that

           A9: [x, y] = [A, { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a }] by A8;

          x = ( [x, y] `1 )

          .= ( [A, { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a }] `1 ) by A9

          .= A;

          hence thesis;

        end;

        for x be object holds x in ( bool the carrier' of C) implies x in ( dom f)

        proof

          let x be object;

          assume x in ( bool the carrier' of C);

          then

          reconsider x as Subset of the carrier' of C;

           [x, { o where o be Object of C : for a be Attribute of C st a in x holds o is-connected-with a }] in f;

          hence thesis by XTUPLE_0:def 12;

        end;

        then

         A10: ( dom f) = ( bool the carrier' of C) by A7, TARSKI: 2;

        ( rng f) c= ( bool the carrier of C)

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A11: [x, y] in f by XTUPLE_0:def 13;

          consider A be Subset of the carrier' of C such that

           A12: [x, y] = [A, { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a }] by A11;

          

           A13: { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a } c= the carrier of C

          proof

            let u be object;

            assume u in { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a };

            then ex u9 be Object of C st u9 = u & for a be Attribute of C st a in A holds u9 is-connected-with a;

            hence thesis;

          end;

          y = ( [x, y] `2 )

          .= ( [A, { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a }] `2 ) by A12

          .= { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a };

          hence thesis by A13;

        end;

        then

        reconsider f as Function of ( bool the carrier' of C), ( bool the carrier of C) by A10, FUNCT_2:def 1, RELSET_1: 4;

        take f;

        for A be Subset of the carrier' of C holds (f . A) = { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a }

        proof

          let A be Subset of the carrier' of C;

          consider y be object such that

           A14: [A, y] in f by A10, XTUPLE_0:def 12;

          consider A9 be Subset of the carrier' of C such that

           A15: [A, y] = [A9, { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a }] by A14;

          

           A16: y = ( [A, y] `2 )

          .= ( [A9, { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a }] `2 ) by A15

          .= { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a };

          A = ( [A, y] `1 )

          .= ( [A9, { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a }] `1 ) by A15

          .= A9;

          hence thesis by A10, A14, A16, FUNCT_1:def 2;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( bool the carrier' of C), ( bool the carrier of C);

        assume

         A17: for A be Subset of the carrier' of C holds (F1 . A) = { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a };

        assume

         A18: for A be Subset of the carrier' of C holds (F2 . A) = { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a };

        

         A19: for A be object st A in ( bool the carrier' of C) holds (F1 . A) = (F2 . A)

        proof

          let A be object;

          assume A in ( bool the carrier' of C);

          then

          reconsider A as Subset of the carrier' of C;

          (F1 . A) = { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a } by A17

          .= (F2 . A) by A18;

          hence thesis;

        end;

        ( dom F1) = ( bool the carrier' of C) & ( dom F2) = ( bool the carrier' of C) by FUNCT_2:def 1;

        hence thesis by A19, FUNCT_1: 2;

      end;

    end

    theorem :: CONLAT_1:1

    for C be FormalContext holds for o be Object of C holds (( ObjectDerivation C) . {o}) = { a where a be Attribute of C : o is-connected-with a }

    proof

      let C be FormalContext;

      let o be Object of C;

       {o} c= the carrier of C

      proof

        let x be object;

        assume x in {o};

        then x = o by TARSKI:def 1;

        hence thesis;

      end;

      then

      reconsider t = {o} as Subset of the carrier of C;

      

       A1: for x be object holds x in { a where a be Attribute of C : for o9 be Object of C st o9 in t holds o9 is-connected-with a } implies x in { a where a be Attribute of C : o is-connected-with a }

      proof

        set o9 = the Element of t;

        let x be object;

        reconsider o9 as Object of C by TARSKI:def 1;

        

         A2: o9 = o by TARSKI:def 1;

        assume x in { a where a be Attribute of C : for o9 be Object of C st o9 in t holds o9 is-connected-with a };

        then

         A3: ex x9 be Attribute of C st x9 = x & for o9 be Object of C st o9 in t holds o9 is-connected-with x9;

        then

        reconsider x as Attribute of C;

        o9 is-connected-with x by A3;

        hence thesis by A2;

      end;

      

       A4: for x be object holds x in { a where a be Attribute of C : o is-connected-with a } implies x in { a where a be Attribute of C : for o9 be Object of C st o9 in t holds o9 is-connected-with a }

      proof

        let x be object;

        assume x in { a where a be Attribute of C : o is-connected-with a };

        then

         A5: ex x9 be Attribute of C st x9 = x & o is-connected-with x9;

        then

        reconsider x as Attribute of C;

        for o9 be Object of C st o9 in t holds o9 is-connected-with x by A5, TARSKI:def 1;

        hence thesis;

      end;

      (( ObjectDerivation C) . t) = { a where a be Attribute of C : for o9 be Object of C st o9 in t holds o9 is-connected-with a } by Def2;

      hence thesis by A1, A4, TARSKI: 2;

    end;

    theorem :: CONLAT_1:2

    for C be FormalContext holds for a be Attribute of C holds (( AttributeDerivation C) . {a}) = { o where o be Object of C : o is-connected-with a }

    proof

      let C be FormalContext;

      let a be Attribute of C;

       {a} c= the carrier' of C

      proof

        let x be object;

        assume x in {a};

        then x = a by TARSKI:def 1;

        hence thesis;

      end;

      then

      reconsider t = {a} as Subset of the carrier' of C;

      

       A1: for x be object holds x in { o where o be Object of C : for a9 be Attribute of C st a9 in t holds o is-connected-with a9 } implies x in { o where o be Object of C : o is-connected-with a }

      proof

        set a9 = the Element of t;

        let x be object;

        reconsider a9 as Attribute of C by TARSKI:def 1;

        

         A2: a9 = a by TARSKI:def 1;

        assume x in { o where o be Object of C : for a9 be Attribute of C st a9 in t holds o is-connected-with a9 };

        then

         A3: ex x9 be Object of C st x9 = x & for a9 be Attribute of C st a9 in t holds x9 is-connected-with a9;

        then

        reconsider x as Object of C;

        x is-connected-with a9 by A3;

        hence thesis by A2;

      end;

      

       A4: for x be object holds x in { o where o be Object of C : o is-connected-with a } implies x in { o where o be Object of C : for a9 be Attribute of C st a9 in t holds o is-connected-with a9 }

      proof

        let x be object;

        assume x in { o where o be Object of C : o is-connected-with a };

        then

         A5: ex x9 be Object of C st x9 = x & x9 is-connected-with a;

        then

        reconsider x as Object of C;

        for a9 be Attribute of C st a9 in t holds x is-connected-with a9 by A5, TARSKI:def 1;

        hence thesis;

      end;

      (( AttributeDerivation C) . t) = { o where o be Object of C : for a9 be Attribute of C st a9 in t holds o is-connected-with a9 } by Def3;

      hence thesis by A1, A4, TARSKI: 2;

    end;

    theorem :: CONLAT_1:3

    

     Th3: for C be FormalContext holds for O1,O2 be Subset of the carrier of C holds O1 c= O2 implies (( ObjectDerivation C) . O2) c= (( ObjectDerivation C) . O1)

    proof

      let C be FormalContext;

      let O1,O2 be Subset of the carrier of C;

      assume

       A1: O1 c= O2;

      let x be object;

      assume x in (( ObjectDerivation C) . O2);

      then x in { a where a be Attribute of C : for o be Object of C st o in O2 holds o is-connected-with a } by Def2;

      then

      consider x9 be Attribute of C such that

       A2: x9 = x and

       A3: for o be Object of C st o in O2 holds o is-connected-with x9;

      for o be Object of C st o in O1 holds o is-connected-with x9 by A1, A3;

      then x in { a where a be Attribute of C : for o be Object of C st o in O1 holds o is-connected-with a } by A2;

      hence thesis by Def2;

    end;

    theorem :: CONLAT_1:4

    

     Th4: for C be FormalContext holds for A1,A2 be Subset of the carrier' of C holds A1 c= A2 implies (( AttributeDerivation C) . A2) c= (( AttributeDerivation C) . A1)

    proof

      let C be FormalContext;

      let A1,A2 be Subset of the carrier' of C;

      assume

       A1: A1 c= A2;

      let x be object;

      assume x in (( AttributeDerivation C) . A2);

      then x in { o where o be Object of C : for a be Attribute of C st a in A2 holds o is-connected-with a } by Def3;

      then

      consider x9 be Object of C such that

       A2: x9 = x and

       A3: for a be Attribute of C st a in A2 holds x9 is-connected-with a;

      for a be Attribute of C st a in A1 holds x9 is-connected-with a by A1, A3;

      then x in { o where o be Object of C : for a be Attribute of C st a in A1 holds o is-connected-with a } by A2;

      hence thesis by Def3;

    end;

    theorem :: CONLAT_1:5

    

     Th5: for C be FormalContext holds for O be Subset of the carrier of C holds O c= (( AttributeDerivation C) . (( ObjectDerivation C) . O))

    proof

      let C be FormalContext;

      let O be Subset of the carrier of C;

      set A = { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a };

      for x be object holds x in A implies x in the carrier' of C

      proof

        let x be object;

        assume x in A;

        then ex x9 be Attribute of C st x9 = x & for o be Object of C st o in O holds o is-connected-with x9;

        hence thesis;

      end;

      then

      reconsider A as Subset of the carrier' of C by TARSKI:def 3;

      let x be object;

      assume

       A1: x in O;

      then

      reconsider x as Object of C;

      

       A2: for a be Attribute of C st a in A holds x is-connected-with a

      proof

        let a be Attribute of C;

        assume a in A;

        then ex a9 be Attribute of C st a9 = a & for o be Object of C st o in O holds o is-connected-with a9;

        hence thesis by A1;

      end;

      (( AttributeDerivation C) . A) = { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a } by Def3;

      then x in (( AttributeDerivation C) . A) by A2;

      hence thesis by Def2;

    end;

    theorem :: CONLAT_1:6

    

     Th6: for C be FormalContext holds for A be Subset of the carrier' of C holds A c= (( ObjectDerivation C) . (( AttributeDerivation C) . A))

    proof

      let C be FormalContext;

      let A be Subset of the carrier' of C;

      set O = { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a };

      for x be object holds x in O implies x in the carrier of C

      proof

        let x be object;

        assume x in O;

        then ex x9 be Object of C st x9 = x & for a be Attribute of C st a in A holds x9 is-connected-with a;

        hence thesis;

      end;

      then

      reconsider O as Subset of the carrier of C by TARSKI:def 3;

      let x be object;

      assume

       A1: x in A;

      then

      reconsider x as Attribute of C;

      

       A2: for o be Object of C st o in O holds o is-connected-with x

      proof

        let o be Object of C;

        assume o in O;

        then ex o9 be Object of C st o9 = o & for a be Attribute of C st a in A holds o9 is-connected-with a;

        hence thesis by A1;

      end;

      (( ObjectDerivation C) . O) = { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a } by Def2;

      then x in (( ObjectDerivation C) . O) by A2;

      hence thesis by Def3;

    end;

    theorem :: CONLAT_1:7

    

     Th7: for C be FormalContext holds for O be Subset of the carrier of C holds (( ObjectDerivation C) . O) = (( ObjectDerivation C) . (( AttributeDerivation C) . (( ObjectDerivation C) . O)))

    proof

      let C be FormalContext;

      let O be Subset of the carrier of C;

      set A = { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a };

      set O9 = { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a };

      set A9 = { a where a be Attribute of C : for o be Object of C st o in O9 holds o is-connected-with a };

      

       A1: for x be object holds x in A9 implies x in A

      proof

        let x be object;

        assume x in A9;

        then

         A2: ex x9 be Attribute of C st x9 = x & for o be Object of C st o in O9 holds o is-connected-with x9;

        then

        reconsider x as Attribute of C;

        for o be Object of C st o in O holds o is-connected-with x

        proof

          let o be Object of C;

          assume

           A3: o in O;

          now

            per cases ;

              case o in O9;

              hence thesis by A2;

            end;

              case not o in O9;

              then

              consider a be Attribute of C such that

               A4: a in A and

               A5: not o is-connected-with a;

              ex a9 be Attribute of C st a9 = a & for o be Object of C st o in O holds o is-connected-with a9 by A4;

              hence thesis by A3, A5;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      for x be object holds x in A implies x in A9

      proof

        let x be object;

        assume

         A6: x in A;

        then ex x9 be Attribute of C st x9 = x & for o be Object of C st o in O holds o is-connected-with x9;

        then

        reconsider x as Attribute of C;

        for o be Object of C st o in O9 holds o is-connected-with x

        proof

          let o be Object of C;

          assume o in O9;

          then ex o9 be Object of C st o9 = o & for a be Attribute of C st a in A holds o9 is-connected-with a;

          hence thesis by A6;

        end;

        hence thesis;

      end;

      then

       A7: A = A9 by A1, TARSKI: 2;

      A c= the carrier' of C

      proof

        let x be object;

        assume x in A;

        then ex x9 be Attribute of C st x9 = x & for o be Object of C st o in O holds o is-connected-with x9;

        hence thesis;

      end;

      then

      reconsider A as Subset of the carrier' of C;

      O9 c= the carrier of C

      proof

        let x be object;

        assume x in O9;

        then ex x9 be Object of C st x9 = x & for a be Attribute of C st a in A holds x9 is-connected-with a;

        hence thesis;

      end;

      then

      reconsider O9 as Subset of the carrier of C;

      A = (( ObjectDerivation C) . O) & O9 = (( AttributeDerivation C) . A) by Def2, Def3;

      hence thesis by A7, Def2;

    end;

    theorem :: CONLAT_1:8

    

     Th8: for C be FormalContext holds for A be Subset of the carrier' of C holds (( AttributeDerivation C) . A) = (( AttributeDerivation C) . (( ObjectDerivation C) . (( AttributeDerivation C) . A)))

    proof

      let C be FormalContext;

      let A be Subset of the carrier' of C;

      set O = { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a };

      set A9 = { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a };

      set O9 = { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a };

      

       A1: for x be object holds x in O9 implies x in O

      proof

        let x be object;

        assume x in O9;

        then

         A2: ex x9 be Object of C st x9 = x & for a be Attribute of C st a in A9 holds x9 is-connected-with a;

        then

        reconsider x as Object of C;

        for a be Attribute of C st a in A holds x is-connected-with a

        proof

          let a be Attribute of C;

          assume

           A3: a in A;

          now

            per cases ;

              case a in A9;

              hence thesis by A2;

            end;

              case not a in A9;

              then

              consider o be Object of C such that

               A4: o in O and

               A5: not o is-connected-with a;

              ex o9 be Object of C st o9 = o & for a be Attribute of C st a in A holds o9 is-connected-with a by A4;

              hence thesis by A3, A5;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      for x be object holds x in O implies x in O9

      proof

        let x be object;

        assume

         A6: x in O;

        then ex x9 be Object of C st x9 = x & for a be Attribute of C st a in A holds x9 is-connected-with a;

        then

        reconsider x as Object of C;

        for a be Attribute of C st a in A9 holds x is-connected-with a

        proof

          let a be Attribute of C;

          assume a in A9;

          then ex a9 be Attribute of C st a9 = a & for o be Object of C st o in O holds o is-connected-with a9;

          hence thesis by A6;

        end;

        hence thesis;

      end;

      then

       A7: O = O9 by A1, TARSKI: 2;

      O c= the carrier of C

      proof

        let x be object;

        assume x in O;

        then ex x9 be Object of C st x9 = x & for a be Attribute of C st a in A holds x9 is-connected-with a;

        hence thesis;

      end;

      then

      reconsider O as Subset of the carrier of C;

      A9 c= the carrier' of C

      proof

        let x be object;

        assume x in A9;

        then ex x9 be Attribute of C st x9 = x & for o be Object of C st o in O holds o is-connected-with x9;

        hence thesis;

      end;

      then

      reconsider A9 as Subset of the carrier' of C;

      O = (( AttributeDerivation C) . A) & A9 = (( ObjectDerivation C) . O) by Def2, Def3;

      hence thesis by A7, Def3;

    end;

    theorem :: CONLAT_1:9

    

     Th9: for C be FormalContext holds for O be Subset of the carrier of C holds for A be Subset of the carrier' of C holds O c= (( AttributeDerivation C) . A) iff [:O, A:] c= the Information of C

    proof

      let C be FormalContext;

      let O be Subset of the carrier of C;

      let A be Subset of the carrier' of C;

      

       A1: [:O, A:] c= the Information of C implies O c= (( AttributeDerivation C) . A)

      proof

        assume

         A2: [:O, A:] c= the Information of C;

        let x be object;

        assume

         A3: x in O;

        then

        reconsider x as Object of C;

        for a be Attribute of C st a in A holds x is-connected-with a

        proof

          let a be Attribute of C;

          consider z be set such that

           A4: z = [x, a];

          assume a in A;

          then z in [:O, A:] by A3, A4, ZFMISC_1:def 2;

          hence thesis by A2, A4;

        end;

        then x in { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a };

        hence thesis by Def3;

      end;

      O c= (( AttributeDerivation C) . A) implies [:O, A:] c= the Information of C

      proof

        assume O c= (( AttributeDerivation C) . A);

        then

         A5: O c= { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a } by Def3;

        let z be object;

        assume z in [:O, A:];

        then

        consider x,y be object such that

         A6: x in O and

         A7: y in A and

         A8: z = [x, y] by ZFMISC_1:def 2;

        reconsider y as Attribute of C by A7;

        reconsider x as Object of C by A6;

        x in { o where o be Object of C : for a be Attribute of C st a in A holds o is-connected-with a } by A5, A6;

        then ex x9 be Object of C st x9 = x & for a be Attribute of C st a in A holds x9 is-connected-with a;

        then x is-connected-with y by A7;

        hence thesis by A8;

      end;

      hence thesis by A1;

    end;

    theorem :: CONLAT_1:10

    

     Th10: for C be FormalContext holds for O be Subset of the carrier of C holds for A be Subset of the carrier' of C holds A c= (( ObjectDerivation C) . O) iff [:O, A:] c= the Information of C

    proof

      let C be FormalContext;

      let O be Subset of the carrier of C;

      let A be Subset of the carrier' of C;

      

       A1: [:O, A:] c= the Information of C implies A c= (( ObjectDerivation C) . O)

      proof

        assume

         A2: [:O, A:] c= the Information of C;

        let x be object;

        assume

         A3: x in A;

        then

        reconsider x as Attribute of C;

        for o be Object of C st o in O holds o is-connected-with x

        proof

          let o be Object of C;

          consider z be set such that

           A4: z = [o, x];

          assume o in O;

          then z in [:O, A:] by A3, A4, ZFMISC_1:def 2;

          hence thesis by A2, A4;

        end;

        then x in { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a };

        hence thesis by Def2;

      end;

      A c= (( ObjectDerivation C) . O) implies [:O, A:] c= the Information of C

      proof

        assume A c= (( ObjectDerivation C) . O);

        then

         A5: A c= { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a } by Def2;

        let z be object;

        assume z in [:O, A:];

        then

        consider x,y be object such that

         A6: x in O and

         A7: y in A and

         A8: z = [x, y] by ZFMISC_1:def 2;

        reconsider y as Attribute of C by A7;

        reconsider x as Object of C by A6;

        y in { a where a be Attribute of C : for o be Object of C st o in O holds o is-connected-with a } by A5, A7;

        then ex y9 be Attribute of C st y9 = y & for o be Object of C st o in O holds o is-connected-with y9;

        then x is-connected-with y by A6;

        hence thesis by A8;

      end;

      hence thesis by A1;

    end;

    theorem :: CONLAT_1:11

    for C be FormalContext holds for O be Subset of the carrier of C holds for A be Subset of the carrier' of C holds O c= (( AttributeDerivation C) . A) iff A c= (( ObjectDerivation C) . O)

    proof

      let C be FormalContext;

      let O be Subset of the carrier of C;

      let A be Subset of the carrier' of C;

      O c= (( AttributeDerivation C) . A) iff [:O, A:] c= the Information of C by Th9;

      hence thesis by Th10;

    end;

    definition

      let C be FormalContext;

      :: CONLAT_1:def5

      func phi (C) -> Function of ( BoolePoset the carrier of C), ( BoolePoset the carrier' of C) equals ( ObjectDerivation C);

      coherence

      proof

        

         A1: ( rng ( ObjectDerivation C)) c= the carrier of ( BoolePoset the carrier' of C)

        proof

          let x be object;

          assume x in ( rng ( ObjectDerivation C));

          then x in ( bool the carrier' of C);

          then

           A2: x in the carrier of ( BooleLatt the carrier' of C) by LATTICE3:def 1;

          ( LattPOSet ( BooleLatt the carrier' of C)) = RelStr (# the carrier of ( BooleLatt the carrier' of C), ( LattRel ( BooleLatt the carrier' of C)) #) by LATTICE3:def 2;

          hence thesis by A2, YELLOW_1:def 2;

        end;

        

         A3: ( LattPOSet ( BooleLatt the carrier of C)) = RelStr (# the carrier of ( BooleLatt the carrier of C), ( LattRel ( BooleLatt the carrier of C)) #) by LATTICE3:def 2;

        

         A4: for x be object holds x in the carrier of ( BoolePoset the carrier of C) implies x in ( dom ( ObjectDerivation C))

        proof

          let x be object;

          assume x in the carrier of ( BoolePoset the carrier of C);

          then x in the carrier of ( LattPOSet ( BooleLatt the carrier of C)) by YELLOW_1:def 2;

          then x in ( bool the carrier of C) by A3, LATTICE3:def 1;

          hence thesis by FUNCT_2:def 1;

        end;

        for x be object holds x in ( dom ( ObjectDerivation C)) implies x in the carrier of ( BoolePoset the carrier of C)

        proof

          let x be object;

          assume x in ( dom ( ObjectDerivation C));

          then x in ( bool the carrier of C);

          then x in the carrier of ( BooleLatt the carrier of C) by LATTICE3:def 1;

          hence thesis by A3, YELLOW_1:def 2;

        end;

        then ( dom ( ObjectDerivation C)) = the carrier of ( BoolePoset the carrier of C) by A4, TARSKI: 2;

        then

        reconsider g = ( ObjectDerivation C) as Function of the carrier of ( BoolePoset the carrier of C), the carrier of ( BoolePoset the carrier' of C) by A1, FUNCT_2:def 1, RELSET_1: 4;

        g is Function of ( BoolePoset the carrier of C), ( BoolePoset the carrier' of C);

        hence thesis;

      end;

    end

    definition

      let C be FormalContext;

      :: CONLAT_1:def6

      func psi (C) -> Function of ( BoolePoset the carrier' of C), ( BoolePoset the carrier of C) equals ( AttributeDerivation C);

      coherence

      proof

        

         A1: ( rng ( AttributeDerivation C)) c= the carrier of ( BoolePoset the carrier of C)

        proof

          let x be object;

          assume x in ( rng ( AttributeDerivation C));

          then x in ( bool the carrier of C);

          then

           A2: x in the carrier of ( BooleLatt the carrier of C) by LATTICE3:def 1;

          ( LattPOSet ( BooleLatt the carrier of C)) = RelStr (# the carrier of ( BooleLatt the carrier of C), ( LattRel ( BooleLatt the carrier of C)) #) by LATTICE3:def 2;

          hence thesis by A2, YELLOW_1:def 2;

        end;

        

         A3: ( LattPOSet ( BooleLatt the carrier' of C)) = RelStr (# the carrier of ( BooleLatt the carrier' of C), ( LattRel ( BooleLatt the carrier' of C)) #) by LATTICE3:def 2;

        

         A4: for x be object holds x in the carrier of ( BoolePoset the carrier' of C) implies x in ( dom ( AttributeDerivation C))

        proof

          let x be object;

          assume x in the carrier of ( BoolePoset the carrier' of C);

          then x in the carrier of ( LattPOSet ( BooleLatt the carrier' of C)) by YELLOW_1:def 2;

          then x in ( bool the carrier' of C) by A3, LATTICE3:def 1;

          hence thesis by FUNCT_2:def 1;

        end;

        for x be object holds x in ( dom ( AttributeDerivation C)) implies x in the carrier of ( BoolePoset the carrier' of C)

        proof

          let x be object;

          assume x in ( dom ( AttributeDerivation C));

          then x in ( bool the carrier' of C);

          then x in the carrier of ( BooleLatt the carrier' of C) by LATTICE3:def 1;

          hence thesis by A3, YELLOW_1:def 2;

        end;

        then ( dom ( AttributeDerivation C)) = the carrier of ( BoolePoset the carrier' of C) by A4, TARSKI: 2;

        hence thesis by A1, FUNCT_2:def 1, RELSET_1: 4;

      end;

    end

    definition

      let P,R be non empty RelStr;

      let Con be Connection of P, R;

      :: CONLAT_1:def7

      attr Con is co-Galois means ex f be Function of P, R, g be Function of R, P st (Con = [f, g] & f is antitone & g is antitone & for p1,p2 be Element of P, r1,r2 be Element of R holds p1 <= (g . (f . p1)) & r1 <= (f . (g . r1)));

    end

    theorem :: CONLAT_1:12

    

     Th12: for P,R be non empty Poset holds for Con be Connection of P, R holds for f be Function of P, R, g be Function of R, P st Con = [f, g] holds Con is co-Galois iff for p be Element of P, r be Element of R holds p <= (g . r) iff r <= (f . p)

    proof

      let P,R be non empty Poset;

      let Con be Connection of P, R;

      let f be Function of P, R, g be Function of R, P;

      assume

       A1: Con = [f, g];

       A2:

      now

        assume

         A3: for p be Element of P, r be Element of R holds p <= (g . r) iff r <= (f . p);

        for p1,p2 be Element of P st p1 <= p2 holds for r1,r2 be Element of R st r1 = (f . p1) & r2 = (f . p2) holds r1 >= r2

        proof

          let p1,p2 be Element of P;

          assume

           A4: p1 <= p2;

          let r1,r2 be Element of R;

          assume

           A5: r1 = (f . p1) & r2 = (f . p2);

          p2 <= (g . (f . p2)) by A3;

          then p1 <= (g . (f . p2)) by A4, ORDERS_2: 3;

          hence thesis by A3, A5;

        end;

        then

         A6: f is antitone by WAYBEL_0:def 5;

        for r1,r2 be Element of R st r1 <= r2 holds for p1,p2 be Element of P st p1 = (g . r1) & p2 = (g . r2) holds p1 >= p2

        proof

          let r1,r2 be Element of R;

          assume

           A7: r1 <= r2;

          let p1,p2 be Element of P;

          assume

           A8: p1 = (g . r1) & p2 = (g . r2);

          r2 <= (f . (g . r2)) by A3;

          then r1 <= (f . (g . r2)) by A7, ORDERS_2: 3;

          hence thesis by A3, A8;

        end;

        then

         A9: g is antitone by WAYBEL_0:def 5;

        for p1,p2 be Element of P, r1,r2 be Element of R holds p1 <= (g . (f . p1)) & r1 <= (f . (g . r1)) by A3;

        hence Con is co-Galois by A1, A6, A9;

      end;

      now

        assume Con is co-Galois;

        then

        consider f9 be Function of P, R, g9 be 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 be Element of P, r1,r2 be Element of R holds p1 <= (g9 . (f9 . p1)) & r1 <= (f9 . (g9 . r1));

        

         A14: g = ( [f, g] `2 )

        .= (Con `2 ) by A1

        .= ( [f9, g9] `2 ) by A10

        .= g9;

        

         A15: f = ( [f, g] `1 )

        .= (Con `1 ) by A1

        .= ( [f9, g9] `1 ) by A10

        .= f9;

        

         A16: for p be Element of P, r be Element of R holds r <= (f . p) implies p <= (g . r)

        proof

          let p be Element of P, r be Element of R;

          assume r <= (f . p);

          then

           A17: (g . r) >= (g . (f . p)) by A12, A14, WAYBEL_0:def 5;

          p <= (g . (f . p)) by A13, A15, A14;

          hence thesis by A17, ORDERS_2: 3;

        end;

        for p be Element of P, r be Element of R holds p <= (g . r) implies r <= (f . p)

        proof

          let p be Element of P, r be Element of R;

          assume p <= (g . r);

          then

           A18: (f . p) >= (f . (g . r)) by A11, A15, WAYBEL_0:def 5;

          r <= (f . (g . r)) by A13, A15, A14;

          hence thesis by A18, ORDERS_2: 3;

        end;

        hence for p be Element of P, r be Element of R holds p <= (g . r) iff r <= (f . p) by A16;

      end;

      hence thesis by A2;

    end;

    theorem :: CONLAT_1:13

    for P,R be non empty Poset holds for Con be Connection of P, R st Con is co-Galois holds for f be Function of P, R, g be Function of R, P st Con = [f, g] holds f = (f * (g * f)) & g = (g * (f * g))

    proof

      let P,R be non empty Poset;

      let Con be Connection of P, R;

      assume Con is co-Galois;

      then

      consider f9 be Function of P, R, g9 be 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 be Element of P, r1,r2 be Element of R holds p1 <= (g9 . (f9 . p1)) & r1 <= (f9 . (g9 . r1));

      let f be Function of P, R, g be Function of R, P;

      assume

       A5: Con = [f, g];

      

       A6: f = ( [f, g] `1 )

      .= (Con `1 ) by A5

      .= ( [f9, g9] `1 ) by A1

      .= f9;

      

       A7: g = ( [f, g] `2 )

      .= (Con `2 ) by A5

      .= ( [f9, g9] `2 ) by A1

      .= g9;

      

       A8: ( dom g) = the carrier of R by FUNCT_2:def 1;

      

       A9: ( dom f) = the carrier of P by FUNCT_2:def 1;

      

       A10: for x be object st x in the carrier of P holds (f . x) = ((f * (g * f)) . x)

      proof

        let x be object;

        assume x in the carrier of P;

        then

        reconsider x as Element of P;

        x <= (g . (f . x)) by A4, A6, A7;

        then

         A11: (f . x) >= (f . (g . (f . x))) by A2, A6, WAYBEL_0:def 5;

        (f . x) <= (f . (g . (f . x))) by A4, A6, A7;

        then (f . x) = (f . (g . (f . x))) by A11, ORDERS_2: 2;

        then

         A12: (f . x) = (f . ((g * f) . x)) by A9, FUNCT_1: 13;

        (f . x) is Element of R;

        then x in ( dom (g * f)) by A9, A8, FUNCT_1: 11;

        hence thesis by A12, FUNCT_1: 13;

      end;

      

       A13: for x be object st x in the carrier of R holds (g . x) = ((g * (f * g)) . x)

      proof

        let x be object;

        assume x in the carrier of R;

        then

        reconsider x as Element of R;

        x <= (f . (g . x)) by A4, A6, A7;

        then

         A14: (g . x) >= (g . (f . (g . x))) by A3, A7, WAYBEL_0:def 5;

        (g . x) <= (g . (f . (g . x))) by A4, A6, A7;

        then (g . x) = (g . (f . (g . x))) by A14, ORDERS_2: 2;

        then

         A15: (g . x) = (g . ((f * g) . x)) by A8, FUNCT_1: 13;

        (g . x) is Element of P;

        then x in ( dom (f * g)) by A9, A8, FUNCT_1: 11;

        hence thesis by A15, FUNCT_1: 13;

      end;

      ( dom (f * (g * f))) = the carrier of P & ( dom (g * (f * g))) = the carrier of R by FUNCT_2:def 1;

      hence thesis by A9, A8, A10, A13, FUNCT_1: 2;

    end;

    theorem :: CONLAT_1:14

    for C be FormalContext holds [( phi C), ( psi C)] is co-Galois

    proof

      let C be FormalContext;

      

       A1: ( LattPOSet ( BooleLatt the carrier' of C)) = RelStr (# the carrier of ( BooleLatt the carrier' of C), ( LattRel ( BooleLatt the carrier' of C)) #) by LATTICE3:def 2;

      

       A2: ( LattPOSet ( BooleLatt the carrier of C)) = RelStr (# the carrier of ( BooleLatt the carrier of C), ( LattRel ( BooleLatt the carrier of C)) #) by LATTICE3:def 2;

      

       A3: for x be Element of ( BoolePoset the carrier of C), y be Element of ( BoolePoset the carrier' of C) st y <= (( phi C) . x) holds x <= (( psi C) . y)

      proof

        let x be Element of ( BoolePoset the carrier of C), y be Element of ( BoolePoset the carrier' of C);

        assume y <= (( phi C) . x);

        then [y, (( phi C) . x)] in the InternalRel of ( BoolePoset the carrier' of C) by ORDERS_2:def 5;

        then

         A4: [y, (( phi C) . x)] in ( LattRel ( BooleLatt the carrier' of C)) by A1, YELLOW_1:def 2;

        reconsider x9 = (( phi C) . x) as Element of ( BooleLatt the carrier' of C) by A1, YELLOW_1:def 2;

        reconsider x as Element of ( BooleLatt the carrier of C) by A2, YELLOW_1:def 2;

        reconsider x as Subset of the carrier of C by LATTICE3:def 1;

        reconsider y as Element of ( BooleLatt the carrier' of C) by A1, YELLOW_1:def 2;

        y [= x9 by A4, FILTER_1: 31;

        then

         A5: (y "\/" x9) = x9 by LATTICES:def 3;

        reconsider x9 as Subset of the carrier' of C by LATTICE3:def 1;

        reconsider y as Subset of the carrier' of C by LATTICE3:def 1;

        for z be object holds z in y implies z in x9 by A5, XBOOLE_0:def 3;

        then y c= x9;

        then

         A6: (( AttributeDerivation C) . x9) c= (( AttributeDerivation C) . y) by Th4;

        reconsider y as Element of ( BoolePoset the carrier' of C);

        reconsider y9 = (( psi C) . y) as Element of ( BooleLatt the carrier of C) by A2, YELLOW_1:def 2;

        reconsider y9 as Subset of the carrier of C by LATTICE3:def 1;

        reconsider y9 as Element of ( BooleLatt the carrier of C);

        

         A7: x c= (( AttributeDerivation C) . (( ObjectDerivation C) . x)) by Th5;

        reconsider x as Subset of the carrier of C;

        reconsider x as Element of ( BooleLatt the carrier of C);

        (x "\/" y9) = y9 by A6, A7, XBOOLE_1: 1, 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 thesis by ORDERS_2:def 5;

      end;

      for x be Element of ( BoolePoset the carrier of C), y be Element of ( BoolePoset the carrier' of C) st x <= (( psi C) . y) holds y <= (( phi C) . x)

      proof

        let x be Element of ( BoolePoset the carrier of C), y be Element of ( BoolePoset the carrier' of C);

        assume x <= (( psi C) . y);

        then [x, (( psi C) . y)] in the InternalRel of ( BoolePoset the carrier of C) by ORDERS_2:def 5;

        then

         A8: [x, (( psi C) . y)] in ( LattRel ( BooleLatt the carrier of C)) by A2, YELLOW_1:def 2;

        reconsider y9 = (( psi C) . y) as Element of ( BooleLatt the carrier of C) by A2, YELLOW_1:def 2;

        reconsider y as Element of ( BooleLatt the carrier' of C) by A1, YELLOW_1:def 2;

        reconsider y as Subset of the carrier' of C by LATTICE3:def 1;

        reconsider x as Element of ( BooleLatt the carrier of C) by A2, YELLOW_1:def 2;

        x [= y9 by A8, FILTER_1: 31;

        then

         A9: (x "\/" y9) = y9 by LATTICES:def 3;

        reconsider y9 as Subset of the carrier of C by LATTICE3:def 1;

        reconsider x as Subset of the carrier of C by LATTICE3:def 1;

        for z be object holds z in x implies z in y9 by A9, XBOOLE_0:def 3;

        then

         A10: x c= y9;

        reconsider x, y9 as Subset of the carrier of C;

        

         A11: (( ObjectDerivation C) . y9) c= (( ObjectDerivation C) . x) by A10, Th3;

        reconsider x as Element of ( BoolePoset the carrier of C);

        reconsider x9 = (( phi C) . x) as Element of ( BooleLatt the carrier' of C) by A1, YELLOW_1:def 2;

        reconsider x9 as Subset of the carrier' of C by LATTICE3:def 1;

        reconsider x9 as Element of ( BooleLatt the carrier' of C);

        

         A12: y c= (( ObjectDerivation C) . (( AttributeDerivation C) . y)) by Th6;

        reconsider y as Element of ( BooleLatt the carrier' of C);

        (y "\/" x9) = x9 by A11, A12, XBOOLE_1: 1, 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 thesis by ORDERS_2:def 5;

      end;

      hence thesis by A3, Th12;

    end;

    theorem :: CONLAT_1:15

    

     Th15: for C be FormalContext holds for O1,O2 be Subset of the carrier of C holds (( ObjectDerivation C) . (O1 \/ O2)) = ((( ObjectDerivation C) . O1) /\ (( ObjectDerivation C) . O2))

    proof

      let C be FormalContext;

      let O1,O2 be Subset of the carrier of C;

      reconsider O9 = (O1 \/ O2) as Subset of the carrier of C;

      

       A1: for x be object holds x in ((( ObjectDerivation C) . O1) /\ (( ObjectDerivation C) . O2)) implies x in (( ObjectDerivation C) . O9)

      proof

        let x be object;

        assume

         A2: x in ((( ObjectDerivation C) . O1) /\ (( ObjectDerivation C) . O2));

        then x in (( ObjectDerivation C) . O1) by XBOOLE_0:def 4;

        then x in { a where a be Attribute of C : for o be Object of C st o in O1 holds o is-connected-with a } by Def2;

        then

         A3: ex x1 be Attribute of C st x1 = x & for o be 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 be Attribute of C : for o be Object of C st o in O2 holds o is-connected-with a } by Def2;

        then

         A4: ex x2 be Attribute of C st x2 = x & for o be Object of C st o in O2 holds o is-connected-with x2;

        then

        reconsider x as Attribute of C;

        for o be Object of C st o in (O1 \/ O2) holds o is-connected-with x

        proof

          let o be Object of C;

          assume

           A5: o in (O1 \/ O2);

          now

            per cases by A5, XBOOLE_0:def 3;

              case o in O1;

              hence thesis by A3;

            end;

              case o in O2;

              hence thesis by A4;

            end;

          end;

          hence thesis;

        end;

        then x in { a where a be Attribute of C : for o be Object of C st o in O9 holds o is-connected-with a };

        hence thesis by Def2;

      end;

      for x be object holds x in (( ObjectDerivation C) . (O1 \/ O2)) implies x in ((( ObjectDerivation C) . O1) /\ (( ObjectDerivation C) . O2))

      proof

        let x be object;

        assume x in (( ObjectDerivation C) . (O1 \/ O2));

        then x in { a where a be Attribute of C : for o be Object of C st o in O9 holds o is-connected-with a } by Def2;

        then

         A6: ex x9 be Attribute of C st x9 = x & for o be Object of C st o in O9 holds o is-connected-with x9;

        then

        reconsider x as Attribute of C;

        for o be Object of C st o in O2 holds o is-connected-with x

        proof

          let o be Object of C;

          assume o in O2;

          then o in O9 by XBOOLE_0:def 3;

          hence thesis by A6;

        end;

        then x in { a where a be Attribute of C : for o be Object of C st o in O2 holds o is-connected-with a };

        then

         A7: x in (( ObjectDerivation C) . O2) by Def2;

        for o be Object of C st o in O1 holds o is-connected-with x

        proof

          let o be Object of C;

          assume o in O1;

          then o in O9 by XBOOLE_0:def 3;

          hence thesis by A6;

        end;

        then x in { a where a be Attribute of C : for o be Object of C st o in O1 holds o is-connected-with a };

        then x in (( ObjectDerivation C) . O1) by Def2;

        hence thesis by A7, XBOOLE_0:def 4;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: CONLAT_1:16

    

     Th16: for C be FormalContext holds for A1,A2 be Subset of the carrier' of C holds (( AttributeDerivation C) . (A1 \/ A2)) = ((( AttributeDerivation C) . A1) /\ (( AttributeDerivation C) . A2))

    proof

      let C be FormalContext;

      let A1,A2 be Subset of the carrier' of C;

      reconsider A9 = (A1 \/ A2) as Subset of the carrier' of C;

      

       A1: for x be object holds x in ((( AttributeDerivation C) . A1) /\ (( AttributeDerivation C) . A2)) implies x in (( AttributeDerivation C) . A9)

      proof

        let x be object;

        assume

         A2: x in ((( AttributeDerivation C) . A1) /\ (( AttributeDerivation C) . A2));

        then x in (( AttributeDerivation C) . A1) by XBOOLE_0:def 4;

        then x in { o where o be Object of C : for a be Attribute of C st a in A1 holds o is-connected-with a } by Def3;

        then

         A3: ex x1 be Object of C st x1 = x & for a be 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 be Object of C : for a be Attribute of C st a in A2 holds o is-connected-with a } by Def3;

        then

         A4: ex x2 be Object of C st x2 = x & for a be Attribute of C st a in A2 holds x2 is-connected-with a;

        then

        reconsider x as Object of C;

        for a be Attribute of C st a in (A1 \/ A2) holds x is-connected-with a

        proof

          let a be Attribute of C;

          assume

           A5: a in (A1 \/ A2);

          now

            per cases by A5, XBOOLE_0:def 3;

              case a in A1;

              hence thesis by A3;

            end;

              case a in A2;

              hence thesis by A4;

            end;

          end;

          hence thesis;

        end;

        then x in { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a };

        hence thesis by Def3;

      end;

      for x be object holds x in (( AttributeDerivation C) . (A1 \/ A2)) implies x in ((( AttributeDerivation C) . A1) /\ (( AttributeDerivation C) . A2))

      proof

        let x be object;

        assume x in (( AttributeDerivation C) . (A1 \/ A2));

        then x in { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a } by Def3;

        then

         A6: ex x9 be Object of C st x9 = x & for a be Attribute of C st a in A9 holds x9 is-connected-with a;

        then

        reconsider x as Object of C;

        for a be Attribute of C st a in A2 holds x is-connected-with a

        proof

          let a be Attribute of C;

          assume a in A2;

          then a in A9 by XBOOLE_0:def 3;

          hence thesis by A6;

        end;

        then x in { o where o be Object of C : for a be Attribute of C st a in A2 holds o is-connected-with a };

        then

         A7: x in (( AttributeDerivation C) . A2) by Def3;

        for a be Attribute of C st a in A1 holds x is-connected-with a

        proof

          let a be Attribute of C;

          assume a in A1;

          then a in A9 by XBOOLE_0:def 3;

          hence thesis by A6;

        end;

        then x in { o where o be Object of C : for a be Attribute of C st a in A1 holds o is-connected-with a };

        then x in (( AttributeDerivation C) . A1) by Def3;

        hence thesis by A7, XBOOLE_0:def 4;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: CONLAT_1:17

    

     Th17: for C be FormalContext holds (( ObjectDerivation C) . {} ) = the carrier' of C

    proof

      let C be FormalContext;

      reconsider e = {} as Subset of the carrier of C by XBOOLE_1: 2;

      set A = { a where a be Attribute of C : for o be Object of C st o in e holds o is-connected-with a };

      

       A1: for x be object holds x in A implies x in the carrier' of C

      proof

        let x be object;

        assume x in A;

        then ex x9 be Attribute of C st x9 = x & for o be Object of C st o in e holds o is-connected-with x9;

        hence thesis;

      end;

      

       A2: for x be object holds x in the carrier' of C implies x in A

      proof

        let x be object;

        assume x in the carrier' of C;

        then

        reconsider x as Attribute of C;

        for o be Object of C st o in e holds o is-connected-with x;

        hence thesis;

      end;

      (( ObjectDerivation C) . e) = { a where a be Attribute of C : for o be Object of C st o in e holds o is-connected-with a } by Def2;

      hence thesis by A1, A2, TARSKI: 2;

    end;

    theorem :: CONLAT_1:18

    

     Th18: for C be FormalContext holds (( AttributeDerivation C) . {} ) = the carrier of C

    proof

      let C be FormalContext;

      reconsider e = {} as Subset of the carrier' of C by XBOOLE_1: 2;

      set O = { o where o be Object of C : for a be Attribute of C st a in e holds o is-connected-with a };

      

       A1: for x be object holds x in O implies x in the carrier of C

      proof

        let x be object;

        assume x in O;

        then ex x9 be Object of C st x9 = x & for a be Attribute of C st a in e holds x9 is-connected-with a;

        hence thesis;

      end;

      

       A2: for x be object holds x in the carrier of C implies x in O

      proof

        let x be object;

        assume x in the carrier of C;

        then

        reconsider x as Object of C;

        for a be Attribute of C st a in e holds x is-connected-with a;

        hence thesis;

      end;

      (( AttributeDerivation C) . e) = { o where o be Object of C : for a be Attribute of C st a in e holds o is-connected-with a } by Def3;

      hence thesis by A1, A2, TARSKI: 2;

    end;

    begin

    definition

      let C be 2-sorted;

      struct ConceptStr over C (# the Extent -> Subset of the carrier of C,

the Intent -> Subset of the carrier' of C #)

       attr strict strict;

    end

    definition

      let C be 2-sorted;

      let CP be ConceptStr over C;

      :: CONLAT_1:def8

      attr CP is empty means

      : Def7: the Extent of CP is empty & the Intent of CP is empty;

      :: CONLAT_1:def9

      attr CP is quasi-empty means

      : Def8: the Extent of CP is empty or the Intent of CP is empty;

    end

    registration

      let C be non empty non void 2-sorted;

      cluster strict non empty for ConceptStr over C;

      existence

      proof

        set A = the non empty Subset of the carrier' of C;

        set O = the non empty Subset of the carrier of C;

         ConceptStr (# O, A #) is non empty;

        hence thesis;

      end;

      cluster strict quasi-empty for ConceptStr over C;

      existence

      proof

        reconsider A = {} as Subset of the carrier' of C by XBOOLE_1: 2;

        reconsider O = {} as Subset of the carrier of C by XBOOLE_1: 2;

         ConceptStr (# O, A #) is quasi-empty;

        hence thesis;

      end;

    end

    registration

      let C be empty void 2-sorted;

      cluster -> empty for ConceptStr over C;

      coherence ;

    end

    

     Lm1: for C be FormalContext holds for CS be ConceptStr over C st (( ObjectDerivation C) . the Extent of CS) = the Intent of CS holds CS is non empty

    proof

      let C be FormalContext;

      let CS be ConceptStr over C;

      assume

       A1: (( ObjectDerivation C) . the Extent of CS) = the Intent of CS;

      now

        per cases ;

          case the Extent of CS is empty;

          then the Intent of CS = the carrier' of C by A1, Th17;

          hence thesis;

        end;

          case the Extent of CS is non empty;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    definition

      let C be FormalContext;

      let CP be ConceptStr over C;

      :: CONLAT_1:def10

      attr CP is concept-like means

      : Def9: (( ObjectDerivation C) . the Extent of CP) = the Intent of CP & (( AttributeDerivation C) . the Intent of CP) = the Extent of CP;

    end

    registration

      let C be FormalContext;

      cluster concept-like non empty for ConceptStr over C;

      existence

      proof

        set o = the Object of C;

        set A = (( ObjectDerivation C) . {o});

         {o} c= the carrier of C

        proof

          let x be object;

          assume x in {o};

          then x = o by TARSKI:def 1;

          hence thesis;

        end;

        then

        reconsider t = {o} as Subset of the carrier of C;

        A c= the carrier' of C

        proof

          let x be object;

          assume x in A;

          then x in { a where a be Attribute of C : for o be Object of C st o in t holds o is-connected-with a } by Def2;

          then ex x9 be Attribute of C st x9 = x & for o be Object of C st o in t holds o is-connected-with x9;

          hence thesis;

        end;

        then

        reconsider A as Subset of the carrier' of C;

        set O = (( AttributeDerivation C) . (( ObjectDerivation C) . {o}));

        O c= the carrier of C

        proof

          let x be object;

          assume x in O;

          then x in { o9 where o9 be Object of C : for a be Attribute of C st a in (( ObjectDerivation C) . t) holds o9 is-connected-with a } by Def3;

          then ex x9 be Object of C st x9 = x & for a be Attribute of C st a in (( ObjectDerivation C) . t) holds x9 is-connected-with a;

          hence thesis;

        end;

        then

        reconsider O as Subset of the carrier of C;

        set M9 = ConceptStr (# O, A #);

        o in {o} & t c= (( AttributeDerivation C) . (( ObjectDerivation C) . t)) by Th5, TARSKI:def 1;

        then

        reconsider M9 as non empty ConceptStr over C by Def7;

        (( ObjectDerivation C) . the Extent of M9) = (( ObjectDerivation C) . t) by Th7

        .= the Intent of M9;

        then M9 is concept-like;

        hence thesis;

      end;

    end

    definition

      let C be FormalContext;

      mode FormalConcept of C is concept-like non empty ConceptStr over C;

    end

    registration

      let C be FormalContext;

      cluster strict for FormalConcept of C;

      existence

      proof

        set CP = the FormalConcept of C;

        

         A1: (( ObjectDerivation C) . the Extent of CP) = the Intent of CP & (( AttributeDerivation C) . the Intent of CP) = the Extent of CP by Def9;

        the Intent of CP is non empty or the Extent of CP is non empty by Def7;

        then the ConceptStr of CP is FormalConcept of C by A1, Def7, Def9;

        hence thesis;

      end;

    end

    theorem :: CONLAT_1:19

    

     Th19: for C be FormalContext holds for O be Subset of the carrier of C holds ConceptStr (# (( AttributeDerivation C) . (( ObjectDerivation C) . O)), (( ObjectDerivation C) . O) #) is FormalConcept of C & for O9 be Subset of the carrier of C, A9 be Subset of the carrier' of C st ConceptStr (# O9, A9 #) is FormalConcept of C & O c= O9 holds (( AttributeDerivation C) . (( ObjectDerivation C) . O)) c= O9

    proof

      let C be FormalContext;

      let O be Subset of the carrier of C;

      

       A1: for O9 be Subset of the carrier of C, A9 be Subset of the carrier' of C st ConceptStr (# O9, A9 #) is FormalConcept of C & O c= O9 holds (( AttributeDerivation C) . (( ObjectDerivation C) . O)) c= O9

      proof

        let O9 be Subset of the carrier of C;

        let A9 be Subset of the carrier' of C;

        assume that

         A2: ConceptStr (# O9, A9 #) is FormalConcept of C and

         A3: O c= O9;

        reconsider M9 = ConceptStr (# O9, A9 #) as FormalConcept of C by A2;

        

         A4: (( AttributeDerivation C) . A9) = the Extent of M9 by Def9

        .= O9;

        

         A5: (( ObjectDerivation C) . O9) = the Intent of M9 by Def9

        .= A9;

        (( ObjectDerivation C) . O9) c= (( ObjectDerivation C) . O) by A3, Th3;

        hence thesis by A4, A5, Th4;

      end;

       ConceptStr (# (( AttributeDerivation C) . (( ObjectDerivation C) . O)), (( ObjectDerivation C) . O) #) is FormalConcept of C

      proof

        set M9 = ConceptStr (# (( AttributeDerivation C) . (( ObjectDerivation C) . O)), (( ObjectDerivation C) . O) #);

        (( ObjectDerivation C) . the Extent of M9) = the Intent of M9 by Th7;

        hence thesis by Def9, Lm1;

      end;

      hence thesis by A1;

    end;

    theorem :: CONLAT_1:20

    for C be FormalContext holds for O be Subset of the carrier of C holds (ex A be Subset of the carrier' of C st ConceptStr (# O, A #) is FormalConcept of C) iff (( AttributeDerivation C) . (( ObjectDerivation C) . O)) = O

    proof

      let C be FormalContext;

      let O be Subset of the carrier of C;

       A1:

      now

        O c= (( AttributeDerivation C) . (( ObjectDerivation C) . O)) by Th5;

        then

         A2: for x be object holds x in O implies x in (( AttributeDerivation C) . (( ObjectDerivation C) . O));

        given A be Subset of the carrier' of C such that

         A3: ConceptStr (# O, A #) is FormalConcept of C;

        (( AttributeDerivation C) . (( ObjectDerivation C) . O)) c= O by A3, Th19;

        then for x be object holds x in (( AttributeDerivation C) . (( ObjectDerivation C) . O)) implies x in O;

        hence (( AttributeDerivation C) . (( ObjectDerivation C) . O)) = O by A2, TARSKI: 2;

      end;

      now

        reconsider A = (( ObjectDerivation C) . O) as Subset of the carrier' of C;

        set M9 = ConceptStr (# O, A #);

        assume (( AttributeDerivation C) . (( ObjectDerivation C) . O)) = O;

        then M9 is FormalConcept of C by Def9, Lm1;

        hence ex A be Subset of the carrier' of C st ConceptStr (# O, A #) is FormalConcept of C;

      end;

      hence thesis by A1;

    end;

    theorem :: CONLAT_1:21

    

     Th21: for C be FormalContext holds for A be Subset of the carrier' of C holds ConceptStr (# (( AttributeDerivation C) . A), (( ObjectDerivation C) . (( AttributeDerivation C) . A)) #) is FormalConcept of C & for O9 be Subset of the carrier of C, A9 be Subset of the carrier' of C st ConceptStr (# O9, A9 #) is FormalConcept of C & A c= A9 holds (( ObjectDerivation C) . (( AttributeDerivation C) . A)) c= A9

    proof

      let C be FormalContext;

      let A be Subset of the carrier' of C;

      

       A1: for O9 be Subset of the carrier of C, A9 be Subset of the carrier' of C st ConceptStr (# O9, A9 #) is FormalConcept of C & A c= A9 holds (( ObjectDerivation C) . (( AttributeDerivation C) . A)) c= A9

      proof

        let O9 be Subset of the carrier of C;

        let A9 be Subset of the carrier' of C;

        assume that

         A2: ConceptStr (# O9, A9 #) is FormalConcept of C and

         A3: A c= A9;

        reconsider M9 = ConceptStr (# O9, A9 #) as FormalConcept of C by A2;

        

         A4: (( AttributeDerivation C) . A9) = the Extent of M9 by Def9

        .= O9;

        

         A5: (( ObjectDerivation C) . O9) = the Intent of M9 by Def9

        .= A9;

        (( AttributeDerivation C) . A9) c= (( AttributeDerivation C) . A) by A3, Th4;

        hence thesis by A4, A5, Th3;

      end;

       ConceptStr (# (( AttributeDerivation C) . A), (( ObjectDerivation C) . (( AttributeDerivation C) . A)) #) is FormalConcept of C

      proof

        set M9 = ConceptStr (# (( AttributeDerivation C) . A), (( ObjectDerivation C) . (( AttributeDerivation C) . A)) #);

        (( AttributeDerivation C) . the Intent of M9) = the Extent of M9 by Th8;

        hence thesis by Def9, Lm1;

      end;

      hence thesis by A1;

    end;

    theorem :: CONLAT_1:22

    for C be FormalContext holds for A be Subset of the carrier' of C holds (ex O be Subset of the carrier of C st ConceptStr (# O, A #) is FormalConcept of C) iff (( ObjectDerivation C) . (( AttributeDerivation C) . A)) = A

    proof

      let C be FormalContext;

      let A be Subset of the carrier' of C;

       A1:

      now

        A c= (( ObjectDerivation C) . (( AttributeDerivation C) . A)) by Th6;

        then

         A2: for x be object holds x in A implies x in (( ObjectDerivation C) . (( AttributeDerivation C) . A));

        given O be Subset of the carrier of C such that

         A3: ConceptStr (# O, A #) is FormalConcept of C;

        (( ObjectDerivation C) . (( AttributeDerivation C) . A)) c= A by A3, Th21;

        then for x be object holds x in (( ObjectDerivation C) . (( AttributeDerivation C) . A)) implies x in A;

        hence (( ObjectDerivation C) . (( AttributeDerivation C) . A)) = A by A2, TARSKI: 2;

      end;

      now

        reconsider O = (( AttributeDerivation C) . A) as Subset of the carrier of C;

        set M9 = ConceptStr (# O, A #);

        assume (( ObjectDerivation C) . (( AttributeDerivation C) . A)) = A;

        then M9 is FormalConcept of C by Def9, Lm1;

        hence ex O be Subset of the carrier of C st ConceptStr (# O, A #) is FormalConcept of C;

      end;

      hence thesis by A1;

    end;

    definition

      let C be FormalContext;

      let CP be ConceptStr over C;

      :: CONLAT_1:def11

      attr CP is universal means the Extent of CP = the carrier of C;

    end

    definition

      let C be FormalContext;

      let CP be ConceptStr over C;

      :: CONLAT_1:def12

      attr CP is co-universal means the Intent of CP = the carrier' of C;

    end

    registration

      let C be FormalContext;

      cluster strict universal for FormalConcept of C;

      existence

      proof

        reconsider e = {} as Subset of the carrier' of C by XBOOLE_1: 2;

        reconsider CP = ConceptStr (# (( AttributeDerivation C) . e), (( ObjectDerivation C) . (( AttributeDerivation C) . e)) #) as FormalConcept of C by Th21;

        (( AttributeDerivation C) . {} ) = the carrier of C by Th18;

        then CP is universal;

        hence thesis;

      end;

      cluster strict co-universal for FormalConcept of C;

      existence

      proof

        reconsider e = {} as Subset of the carrier of C by XBOOLE_1: 2;

        reconsider CP = ConceptStr (# (( AttributeDerivation C) . (( ObjectDerivation C) . e)), (( ObjectDerivation C) . e) #) as FormalConcept of C by Th19;

        (( ObjectDerivation C) . {} ) = the carrier' of C by Th17;

        then CP is co-universal;

        hence thesis;

      end;

    end

    definition

      let C be FormalContext;

      :: CONLAT_1:def13

      func Concept-with-all-Objects (C) -> strict universal FormalConcept of C means

      : Def12: ex O be Subset of the carrier of C, A be Subset of the carrier' of C st it = ConceptStr (# O, A #) & O = (( AttributeDerivation C) . {} ) & A = (( ObjectDerivation C) . (( AttributeDerivation C) . {} ));

      existence

      proof

        reconsider e = {} as Subset of the carrier' of C by XBOOLE_1: 2;

        reconsider CP = ConceptStr (# (( AttributeDerivation C) . e), (( ObjectDerivation C) . (( AttributeDerivation C) . e)) #) as FormalConcept of C by Th21;

        (( AttributeDerivation C) . {} ) = the carrier of C by Th18;

        then CP is universal;

        hence thesis;

      end;

      uniqueness ;

    end

    definition

      let C be FormalContext;

      :: CONLAT_1:def14

      func Concept-with-all-Attributes (C) -> strict co-universal FormalConcept of C means

      : Def13: ex O be Subset of the carrier of C, A be Subset of the carrier' of C st it = ConceptStr (# O, A #) & O = (( AttributeDerivation C) . (( ObjectDerivation C) . {} )) & A = (( ObjectDerivation C) . {} );

      existence

      proof

        reconsider e = {} as Subset of the carrier of C by XBOOLE_1: 2;

        reconsider CP = ConceptStr (# (( AttributeDerivation C) . (( ObjectDerivation C) . e)), (( ObjectDerivation C) . e) #) as FormalConcept of C by Th19;

        (( ObjectDerivation C) . {} ) = the carrier' of C by Th17;

        then CP is co-universal;

        hence thesis;

      end;

      uniqueness ;

    end

    theorem :: CONLAT_1:23

    

     Th23: for C be FormalContext holds the Extent of ( Concept-with-all-Objects C) = the carrier of C & the Intent of ( Concept-with-all-Attributes C) = the carrier' of C

    proof

      let C be FormalContext;

      (ex O be Subset of the carrier of C, A be 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 be Subset of the carrier of C, A be Subset of the carrier' of C st ( Concept-with-all-Attributes C) = ConceptStr (# O, A #) & O = (( AttributeDerivation C) . (( ObjectDerivation C) . {} )) & A = (( ObjectDerivation C) . {} ) by Def12, Def13;

      hence thesis by Th17, Th18;

    end;

    theorem :: CONLAT_1:24

    for C be FormalContext holds for CP be FormalConcept of C holds (the Extent of CP = {} implies CP is co-universal) & (the Intent of CP = {} implies CP is universal)

    proof

      let C be FormalContext;

      let CP be FormalConcept of C;

      

       A1: (( AttributeDerivation C) . the Intent of CP) = the Extent of CP by Def9;

      

       A2: the Intent of CP = {} implies CP is universal by A1, Th18;

      

       A3: (( ObjectDerivation C) . the Extent of CP) = the Intent of CP by Def9;

      the Extent of CP = {} implies CP is co-universal by A3, Th17;

      hence thesis by A2;

    end;

    theorem :: CONLAT_1:25

    

     Th25: for C be FormalContext holds for CP be strict FormalConcept of C holds (the Extent of CP = {} implies CP = ( Concept-with-all-Attributes C)) & (the Intent of CP = {} implies CP = ( Concept-with-all-Objects C))

    proof

      let C be FormalContext;

      let CP be strict FormalConcept of C;

      

       A1: (( AttributeDerivation C) . the Intent of CP) = the Extent of CP by Def9;

      

       A2: (( ObjectDerivation C) . the Extent of CP) = the Intent of CP by Def9;

       A3:

      now

        assume

         A4: the Intent of CP = {} ;

        then the Extent of CP = the carrier of C by A1, Th18;

        then CP is universal;

        hence CP = ( Concept-with-all-Objects C) by A2, A1, A4, Def12;

      end;

      now

        assume

         A5: the Extent of CP = {} ;

        then the Intent of CP = the carrier' of C by A2, Th17;

        then CP is co-universal;

        hence CP = ( Concept-with-all-Attributes C) by A2, A1, A5, Def13;

      end;

      hence thesis by A3;

    end;

    theorem :: CONLAT_1:26

    for C be FormalContext holds for CP be quasi-empty ConceptStr over C st CP is FormalConcept of C holds CP is universal or CP is co-universal

    proof

      let C be FormalContext;

      let CP be quasi-empty ConceptStr over C;

      assume CP is FormalConcept of C;

      then

      reconsider CP as FormalConcept of C;

      

       A1: (( AttributeDerivation C) . the Intent of CP) = the Extent of CP by Def9;

      

       A2: (( ObjectDerivation C) . the Extent of CP) = the Intent of CP by Def9;

      now

        per cases by Def8;

          case the Intent of CP is empty;

          then the Extent of CP = the carrier of C by A1, Th18;

          hence CP is universal;

        end;

          case the Extent of CP is empty;

          then the Intent of CP = the carrier' of C by A2, Th17;

          hence CP is co-universal;

        end;

      end;

      hence thesis;

    end;

    theorem :: CONLAT_1:27

    for C be FormalContext holds for CP be quasi-empty ConceptStr over C st CP is strict FormalConcept of C holds CP = ( Concept-with-all-Objects C) or CP = ( Concept-with-all-Attributes C)

    proof

      let C be FormalContext;

      let CP be quasi-empty ConceptStr over C;

      assume

       A1: CP is strict FormalConcept of C;

      now

        per cases by Def8;

          case the Intent of CP is empty;

          hence CP = ( Concept-with-all-Objects C) by A1, Th25;

        end;

          case the Extent of CP is empty;

          hence CP = ( Concept-with-all-Attributes C) by A1, Th25;

        end;

      end;

      hence thesis;

    end;

    definition

      let C be FormalContext;

      :: CONLAT_1:def15

      mode Set-of-FormalConcepts of C -> non empty set means

      : Def14: for X be set st X in it holds X is FormalConcept of C;

      existence

      proof

        set CP = the FormalConcept of C;

        for X be set st X in {CP} holds X is FormalConcept of C by TARSKI:def 1;

        hence thesis;

      end;

    end

    definition

      let C be FormalContext;

      let FCS be Set-of-FormalConcepts of C;

      :: original: Element

      redefine

      mode Element of FCS -> FormalConcept of C ;

      coherence by Def14;

    end

    definition

      let C be FormalContext;

      let CP1,CP2 be FormalConcept of C;

      :: CONLAT_1:def16

      pred CP1 is-SubConcept-of CP2 means the Extent of CP1 c= the Extent of CP2;

    end

    notation

      let C be FormalContext;

      let CP1,CP2 be FormalConcept of C;

      synonym CP2 is-SuperConcept-of CP1 for CP1 is-SubConcept-of CP2;

    end

    theorem :: CONLAT_1:28

    

     Th28: for C be FormalContext holds for CP1,CP2 be FormalConcept of C holds CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1

    proof

      let C be FormalContext;

      let CP1,CP2 be FormalConcept of C;

       A1:

      now

        assume the Intent of CP2 c= the Intent of CP1;

        then

         A2: (( AttributeDerivation C) . the Intent of CP1) c= (( AttributeDerivation C) . the Intent of CP2) by Th4;

        (( AttributeDerivation C) . the Intent of CP1) = the Extent of CP1 & (( AttributeDerivation C) . the Intent of CP2) = the Extent of CP2 by Def9;

        hence CP1 is-SubConcept-of CP2 by A2;

      end;

      now

        assume CP1 is-SubConcept-of CP2;

        then

         A3: the Extent of CP1 c= the Extent of CP2;

        (( ObjectDerivation C) . the Extent of CP2) = the Intent of CP2 & (( ObjectDerivation C) . the Extent of CP1) = the Intent of CP1 by Def9;

        hence the Intent of CP2 c= the Intent of CP1 by A3, Th3;

      end;

      hence thesis by A1;

    end;

    theorem :: CONLAT_1:29

    for C be FormalContext holds for CP1,CP2 be 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 be FormalContext holds for CP be FormalConcept of C holds CP is-SubConcept-of ( Concept-with-all-Objects C) & ( Concept-with-all-Attributes C) is-SubConcept-of CP

    proof

      let C be FormalContext;

      let CP be FormalConcept of C;

      

       A1: the carrier' of C = the Intent of ( Concept-with-all-Attributes C) & the Intent of CP c= the carrier' of C by Th23;

      the carrier of C = the Extent of ( Concept-with-all-Objects C) & the Extent of CP c= the carrier of C by Th23;

      hence thesis by A1, Th28;

    end;

    begin

    definition

      let C be FormalContext;

      :: CONLAT_1:def17

      func B-carrier (C) -> non empty set equals { ConceptStr (# E, I #) where E be Subset of the carrier of C, I be Subset of the carrier' of C : ConceptStr (# E, I #) is non empty & (( ObjectDerivation C) . E) = I & (( AttributeDerivation C) . I) = E };

      coherence

      proof

        set M9 = { ConceptStr (# E, I #) where E be Subset of the carrier of C, I be Subset of the carrier' of C : ConceptStr (# E, I #) is non empty & (( ObjectDerivation C) . E) = I & (( AttributeDerivation C) . I) = E };

        M9 is non empty

        proof

          set CP = the FormalConcept of C;

          consider O be Subset of the carrier of C such that

           A1: O = the Extent of CP;

          consider A be Subset of the carrier' of C such that

           A2: A = the Intent of CP;

          

           A3: (( AttributeDerivation C) . A) = O by A1, A2, Def9;

          

           A4: (( ObjectDerivation C) . O) = A by A1, A2, Def9;

          then ConceptStr (# O, A #) is non empty by Lm1;

          then ConceptStr (# O, A #) in M9 by A4, A3;

          hence thesis;

        end;

        then

        reconsider M9 as non empty set;

        for CP be strict non empty ConceptStr over C holds CP in M9 iff (( ObjectDerivation C) . the Extent of CP) = the Intent of CP & (( AttributeDerivation C) . the Intent of CP) = the Extent of CP

        proof

          let CP be strict non empty ConceptStr over C;

          now

            assume CP in M9;

            then ex E be Subset of the carrier of C, I be Subset of the carrier' of C st CP = ConceptStr (# E, I #) & ConceptStr (# E, I #) is non empty & (( ObjectDerivation C) . E) = I & (( AttributeDerivation C) . I) = E;

            hence (( ObjectDerivation C) . the Extent of CP) = the Intent of CP & (( AttributeDerivation C) . the Intent of CP) = the Extent of CP;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let C be FormalContext;

      :: original: B-carrier

      redefine

      func B-carrier (C) -> Set-of-FormalConcepts of C ;

      coherence

      proof

        for X be set holds X in ( B-carrier C) implies X is FormalConcept of C

        proof

          let X be set;

          assume X in ( B-carrier C);

          then ex E be Subset of the carrier of C, I be Subset of the carrier' of C st X = ConceptStr (# E, I #) & ConceptStr (# E, I #) is non empty & (( ObjectDerivation C) . E) = I & (( AttributeDerivation C) . I) = E;

          hence thesis by Def9;

        end;

        hence thesis by Def14;

      end;

    end

    registration

      let C be FormalContext;

      cluster ( B-carrier C) -> non empty;

      coherence ;

    end

    theorem :: CONLAT_1:31

    

     Th31: for C be FormalContext holds for CP be object holds CP in ( B-carrier C) iff CP is strict FormalConcept of C

    proof

      let C be FormalContext;

      let CP be object;

      

       A1: CP is strict FormalConcept of C implies CP in ( B-carrier C)

      proof

        assume

         A2: CP is strict FormalConcept of C;

        then

        reconsider CP as FormalConcept of C;

        set I9 = the Intent of CP;

        set E9 = the Extent of CP;

        (( ObjectDerivation C) . E9) = I9 & (( AttributeDerivation C) . I9) = E9 by Def9;

        hence thesis by A2;

      end;

      CP in ( B-carrier C) implies CP is strict FormalConcept of C

      proof

        assume CP in ( B-carrier C);

        then ex E be Subset of the carrier of C, I be Subset of the carrier' of C st CP = ConceptStr (# E, I #) & ConceptStr (# E, I #) is non empty & (( ObjectDerivation C) . E) = I & (( AttributeDerivation C) . I) = E;

        hence thesis by Def9;

      end;

      hence thesis by A1;

    end;

    definition

      let C be FormalContext;

      :: CONLAT_1:def18

      func B-meet (C) -> BinOp of ( B-carrier C) means

      : Def17: for CP1,CP2 be strict FormalConcept of C holds ex O be Subset of the carrier of C, A be Subset of the carrier' of C st (it . (CP1,CP2)) = ConceptStr (# O, A #) & O = (the Extent of CP1 /\ the Extent of CP2) & A = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP2)));

      existence

      proof

        defpred P[ FormalConcept of C, FormalConcept of C, set] means ex O be Subset of the carrier of C, A be 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 be Element of ( B-carrier C), CP2 be Element of ( B-carrier C) holds ex CP be Element of ( B-carrier C) st P[CP1, CP2, CP]

        proof

          let CP1 be Element of ( B-carrier C);

          let CP2 be Element of ( B-carrier C);

          set O = (the Extent of CP1 /\ the Extent of CP2);

          set A = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP2)));

          reconsider A9 = (the Intent of CP1 \/ the Intent of CP2) as Subset of the carrier' of C;

          set CP = ConceptStr (# O, A #);

          

           A2: (( AttributeDerivation C) . A) = (( AttributeDerivation C) . A9) by Th8

          .= ((( AttributeDerivation C) . the Intent of CP1) /\ (( AttributeDerivation C) . the Intent of CP2)) by Th16

          .= (the Extent of CP1 /\ (( AttributeDerivation C) . the Intent of CP2)) by Def9

          .= (the Extent of CP1 /\ the Extent of CP2) by Def9;

          then

           A3: (( ObjectDerivation C) . O) = A by Th7;

          then ConceptStr (# O, A #) is non empty by Lm1;

          then CP in { ConceptStr (# E, I #) where E be Subset of the carrier of C, I be Subset of the carrier' of C : ConceptStr (# E, I #) is non empty & (( ObjectDerivation C) . E) = I & (( AttributeDerivation C) . I) = E } by A2, A3;

          hence thesis;

        end;

        consider f be Function of [:( B-carrier C), ( B-carrier C):], ( B-carrier C) such that

         A4: for CP1 be Element of ( B-carrier C), CP2 be Element of ( B-carrier C) holds P[CP1, CP2, (f . (CP1,CP2))] from BINOP_1:sch 3( A1);

        reconsider f as BinOp of ( B-carrier C);

        take f;

        for CP1,CP2 be strict FormalConcept of C holds ex O be Subset of the carrier of C, A be Subset of the carrier' of C st (f . (CP1,CP2)) = ConceptStr (# O, A #) & O = (the Extent of CP1 /\ the Extent of CP2) & A = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP2)))

        proof

          let CP1,CP2 be strict FormalConcept of C;

          CP1 is Element of ( B-carrier C) & CP2 is Element of ( B-carrier C) by Th31;

          hence thesis by A4;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be BinOp of ( B-carrier C);

        assume

         A5: for CP1,CP2 be strict FormalConcept of C holds ex O be Subset of the carrier of C, A be Subset of the carrier' of C st (F1 . (CP1,CP2)) = ConceptStr (# O, A #) & O = (the Extent of CP1 /\ the Extent of CP2) & A = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP2)));

        assume

         A6: for CP1,CP2 be strict FormalConcept of C holds ex O be Subset of the carrier of C, A be Subset of the carrier' of C st (F2 . (CP1,CP2)) = ConceptStr (# O, A #) & O = (the Extent of CP1 /\ the Extent of CP2) & A = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP2)));

        

         A7: for X be object st X in [:( B-carrier C), ( B-carrier C):] holds (F1 . X) = (F2 . X)

        proof

          let X be object;

          assume X in [:( B-carrier C), ( B-carrier C):];

          then

          consider A,B be object such that

           A8: A in ( B-carrier C) and

           A9: B in ( B-carrier C) and

           A10: X = [A, B] by ZFMISC_1:def 2;

          reconsider B as strict FormalConcept of C by A9, Th31;

          reconsider A as strict FormalConcept of C by A8, Th31;

          (ex O be Subset of the carrier of C, At be 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 be Subset of the carrier of C, At9 be Subset of the carrier' of C st (F2 . (A,B)) = ConceptStr (# O9, At9 #) & O9 = (the Extent of A /\ the Extent of B) & At9 = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of A \/ the Intent of B))) by A5, A6;

          hence thesis by A10;

        end;

        ( dom F1) = [:( B-carrier C), ( B-carrier C):] & ( dom F2) = [:( B-carrier C), ( B-carrier C):] by FUNCT_2:def 1;

        hence thesis by A7, FUNCT_1: 2;

      end;

    end

    definition

      let C be FormalContext;

      :: CONLAT_1:def19

      func B-join (C) -> BinOp of ( B-carrier C) means

      : Def18: for CP1,CP2 be strict FormalConcept of C holds ex O be Subset of the carrier of C, A be Subset of the carrier' of C st (it . (CP1,CP2)) = ConceptStr (# O, A #) & O = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))) & A = (the Intent of CP1 /\ the Intent of CP2);

      existence

      proof

        defpred P[ FormalConcept of C, FormalConcept of C, set] means ex O be Subset of the carrier of C, A be 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 be Element of ( B-carrier C), CP2 be Element of ( B-carrier C) holds ex CP be Element of ( B-carrier C) st P[CP1, CP2, CP]

        proof

          let CP1 be Element of ( B-carrier C);

          let CP2 be Element of ( B-carrier C);

          set O = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)));

          set A = (the Intent of CP1 /\ the Intent of CP2);

          reconsider O9 = (the Extent of CP1 \/ the Extent of CP2) as Subset of the carrier of C;

          set CP = ConceptStr (# O, A #);

          

           A2: (( ObjectDerivation C) . O) = (( ObjectDerivation C) . O9) by Th7

          .= ((( ObjectDerivation C) . the Extent of CP1) /\ (( ObjectDerivation C) . the Extent of CP2)) by Th15

          .= (the Intent of CP1 /\ (( ObjectDerivation C) . the Extent of CP2)) by Def9

          .= (the Intent of CP1 /\ the Intent of CP2) by Def9;

          then (( AttributeDerivation C) . A) = O & ConceptStr (# O, A #) is non empty by Lm1, Th7;

          then CP in { ConceptStr (# E, I #) where E be Subset of the carrier of C, I be Subset of the carrier' of C : ConceptStr (# E, I #) is non empty & (( ObjectDerivation C) . E) = I & (( AttributeDerivation C) . I) = E } by A2;

          hence thesis;

        end;

        consider f be Function of [:( B-carrier C), ( B-carrier C):], ( B-carrier C) such that

         A3: for CP1 be Element of ( B-carrier C), CP2 be Element of ( B-carrier C) holds P[CP1, CP2, (f . (CP1,CP2))] from BINOP_1:sch 3( A1);

        reconsider f as BinOp of ( B-carrier C);

        take f;

        for CP1,CP2 be strict FormalConcept of C holds ex O be Subset of the carrier of C, A be Subset of the carrier' of C st (f . (CP1,CP2)) = ConceptStr (# O, A #) & O = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))) & A = (the Intent of CP1 /\ the Intent of CP2)

        proof

          let CP1,CP2 be strict FormalConcept of C;

          CP1 is Element of ( B-carrier C) & CP2 is Element of ( B-carrier C) by Th31;

          hence thesis by A3;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be BinOp of ( B-carrier C);

        assume

         A4: for CP1,CP2 be strict FormalConcept of C holds ex O be Subset of the carrier of C, A be Subset of the carrier' of C st (F1 . (CP1,CP2)) = ConceptStr (# O, A #) & O = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))) & A = (the Intent of CP1 /\ the Intent of CP2);

        assume

         A5: for CP1,CP2 be strict FormalConcept of C holds ex O be Subset of the carrier of C, A be Subset of the carrier' of C st (F2 . (CP1,CP2)) = ConceptStr (# O, A #) & O = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))) & A = (the Intent of CP1 /\ the Intent of CP2);

        

         A6: for X be object st X in [:( B-carrier C), ( B-carrier C):] holds (F1 . X) = (F2 . X)

        proof

          let X be object;

          assume X in [:( B-carrier C), ( B-carrier C):];

          then

          consider A,B be object such that

           A7: A in ( B-carrier C) and

           A8: B in ( B-carrier C) and

           A9: X = [A, B] by ZFMISC_1:def 2;

          reconsider B as strict FormalConcept of C by A8, Th31;

          reconsider A as strict FormalConcept of C by A7, Th31;

          (ex O be Subset of the carrier of C, At be 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 be Subset of the carrier of C, At9 be Subset of the carrier' of C st (F2 . (A,B)) = ConceptStr (# O9, At9 #) & O9 = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of A \/ the Extent of B))) & At9 = (the Intent of A /\ the Intent of B) by A4, A5;

          hence thesis by A9;

        end;

        ( dom F1) = [:( B-carrier C), ( B-carrier C):] & ( dom F2) = [:( B-carrier C), ( B-carrier C):] by FUNCT_2:def 1;

        hence thesis by A6, FUNCT_1: 2;

      end;

    end

    

     Lm2: for C be FormalContext holds for CP1,CP2 be strict FormalConcept of C holds (( B-meet C) . (CP1,CP2)) in ( rng ( B-meet C))

    proof

      let C be FormalContext;

      let CP1,CP2 be strict FormalConcept of C;

      CP1 in ( B-carrier C) & CP2 in ( B-carrier C) by Th31;

      then [CP1, CP2] in [:( B-carrier C), ( B-carrier C):] by ZFMISC_1:def 2;

      then [CP1, CP2] in ( dom ( B-meet C)) by FUNCT_2:def 1;

      hence thesis by FUNCT_1:def 3;

    end;

    

     Lm3: for C be FormalContext holds for CP1,CP2 be strict FormalConcept of C holds (( B-join C) . (CP1,CP2)) in ( rng ( B-join C))

    proof

      let C be FormalContext;

      let CP1,CP2 be strict FormalConcept of C;

      CP1 in ( B-carrier C) & CP2 in ( B-carrier C) by Th31;

      then [CP1, CP2] in [:( B-carrier C), ( B-carrier C):] by ZFMISC_1:def 2;

      then [CP1, CP2] in ( dom ( B-join C)) by FUNCT_2:def 1;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: CONLAT_1:32

    

     Th32: for C be FormalContext holds for CP1,CP2 be strict FormalConcept of C holds (( B-meet C) . (CP1,CP2)) = (( B-meet C) . (CP2,CP1))

    proof

      let C be FormalContext;

      let CP1,CP2 be strict FormalConcept of C;

      (ex O be Subset of the carrier of C, A be 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 be Subset of the carrier of C, A9 be Subset of the carrier' of C st (( B-meet C) . (CP2,CP1)) = ConceptStr (# O9, A9 #) & O9 = (the Extent of CP2 /\ the Extent of CP1) & A9 = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP2 \/ the Intent of CP1))) by Def17;

      hence thesis;

    end;

    theorem :: CONLAT_1:33

    

     Th33: for C be FormalContext holds for CP1,CP2 be strict FormalConcept of C holds (( B-join C) . (CP1,CP2)) = (( B-join C) . (CP2,CP1))

    proof

      let C be FormalContext;

      let CP1,CP2 be strict FormalConcept of C;

      (ex O be Subset of the carrier of C, A be 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 be Subset of the carrier of C, A9 be Subset of the carrier' of C st (( B-join C) . (CP2,CP1)) = ConceptStr (# O9, A9 #) & O9 = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP2 \/ the Extent of CP1))) & A9 = (the Intent of CP2 /\ the Intent of CP1) by Def18;

      hence thesis;

    end;

    theorem :: CONLAT_1:34

    

     Th34: for C be FormalContext holds for CP1,CP2,CP3 be strict FormalConcept of C holds (( B-meet C) . (CP1,(( B-meet C) . (CP2,CP3)))) = (( B-meet C) . ((( B-meet C) . (CP1,CP2)),CP3))

    proof

      let C be FormalContext;

      let CP1,CP2,CP3 be strict FormalConcept of C;

      (( B-meet C) . (CP1,CP2)) in ( rng ( B-meet C)) by Lm2;

      then

      reconsider CP = (( B-meet C) . (CP1,CP2)) as strict FormalConcept of C by Th31;

      

       A1: (ex O be Subset of the carrier of C, A be 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 be Subset of the carrier of C, A9 be Subset of the carrier' of C st (( B-meet C) . (CP,CP3)) = ConceptStr (# O9, A9 #) & O9 = (the Extent of CP /\ the Extent of CP3) & A9 = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP \/ the Intent of CP3))) by Def17;

      (( B-meet C) . (CP2,CP3)) in ( rng ( B-meet C)) by Lm2;

      then

      reconsider CP9 = (( B-meet C) . (CP2,CP3)) as strict FormalConcept of C by Th31;

      

       A2: (ex O be Subset of the carrier of C, A be 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 be Subset of the carrier of C, A9 be Subset of the carrier' of C st (( B-meet C) . (CP1,CP9)) = ConceptStr (# O9, A9 #) & O9 = (the Extent of CP1 /\ the Extent of CP9) & A9 = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP9))) by Def17;

      (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP2 \/ the Intent of CP3)))))) = (( ObjectDerivation C) . ((( AttributeDerivation C) . the Intent of CP1) /\ (( AttributeDerivation C) . (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP2 \/ the Intent of CP3)))))) by Th16

      .= (( ObjectDerivation C) . ((( AttributeDerivation C) . the Intent of CP1) /\ (( AttributeDerivation C) . (the Intent of CP2 \/ the Intent of CP3)))) by Th8

      .= (( ObjectDerivation C) . ((( AttributeDerivation C) . the Intent of CP1) /\ ((( AttributeDerivation C) . the Intent of CP2) /\ (( AttributeDerivation C) . the Intent of CP3)))) by Th16

      .= (( ObjectDerivation C) . (((( AttributeDerivation C) . the Intent of CP1) /\ (( AttributeDerivation C) . the Intent of CP2)) /\ (( AttributeDerivation C) . the Intent of CP3))) by XBOOLE_1: 16

      .= (( ObjectDerivation C) . ((( AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP2)) /\ (( AttributeDerivation C) . the Intent of CP3))) by Th16

      .= (( ObjectDerivation C) . ((( AttributeDerivation C) . (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP2)))) /\ (( AttributeDerivation C) . the Intent of CP3))) by Th8

      .= (( ObjectDerivation C) . (( AttributeDerivation C) . ((( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP2))) \/ the Intent of CP3))) by Th16;

      hence thesis by A1, A2, XBOOLE_1: 16;

    end;

    theorem :: CONLAT_1:35

    

     Th35: for C be FormalContext holds for CP1,CP2,CP3 be strict FormalConcept of C holds (( B-join C) . (CP1,(( B-join C) . (CP2,CP3)))) = (( B-join C) . ((( B-join C) . (CP1,CP2)),CP3))

    proof

      let C be FormalContext;

      let CP1,CP2,CP3 be strict FormalConcept of C;

      (( B-join C) . (CP1,CP2)) in ( rng ( B-join C)) by Lm3;

      then

      reconsider CP = (( B-join C) . (CP1,CP2)) as strict FormalConcept of C by Th31;

      

       A1: (ex O be Subset of the carrier of C, A be 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 be Subset of the carrier of C, A9 be Subset of the carrier' of C st (( B-join C) . (CP,CP3)) = ConceptStr (# O9, A9 #) & O9 = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP \/ the Extent of CP3))) & A9 = (the Intent of CP /\ the Intent of CP3) by Def18;

      (( B-join C) . (CP2,CP3)) in ( rng ( B-join C)) by Lm3;

      then

      reconsider CP9 = (( B-join C) . (CP2,CP3)) as strict FormalConcept of C by Th31;

      

       A2: (ex O be Subset of the carrier of C, A be 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 be Subset of the carrier of C, A9 be Subset of the carrier' of C st (( B-join C) . (CP1,CP9)) = ConceptStr (# O9, A9 #) & O9 = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP9))) & A9 = (the Intent of CP1 /\ the Intent of CP9) by Def18;

      (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP1 \/ (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP2 \/ the Extent of CP3)))))) = (( AttributeDerivation C) . ((( ObjectDerivation C) . the Extent of CP1) /\ (( ObjectDerivation C) . (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP2 \/ the Extent of CP3)))))) by Th15

      .= (( AttributeDerivation C) . ((( ObjectDerivation C) . the Extent of CP1) /\ (( ObjectDerivation C) . (the Extent of CP2 \/ the Extent of CP3)))) by Th7

      .= (( AttributeDerivation C) . ((( ObjectDerivation C) . the Extent of CP1) /\ ((( ObjectDerivation C) . the Extent of CP2) /\ (( ObjectDerivation C) . the Extent of CP3)))) by Th15

      .= (( AttributeDerivation C) . (((( ObjectDerivation C) . the Extent of CP1) /\ (( ObjectDerivation C) . the Extent of CP2)) /\ (( ObjectDerivation C) . the Extent of CP3))) by XBOOLE_1: 16

      .= (( AttributeDerivation C) . ((( ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) /\ (( ObjectDerivation C) . the Extent of CP3))) by Th15

      .= (( AttributeDerivation C) . ((( ObjectDerivation C) . (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)))) /\ (( ObjectDerivation C) . the Extent of CP3))) by Th7

      .= (( AttributeDerivation C) . (( ObjectDerivation C) . ((( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))) \/ the Extent of CP3))) by Th15;

      hence thesis by A1, A2, XBOOLE_1: 16;

    end;

    theorem :: CONLAT_1:36

    

     Th36: for C be FormalContext holds for CP1,CP2 be strict FormalConcept of C holds (( B-join C) . ((( B-meet C) . (CP1,CP2)),CP2)) = CP2

    proof

      let C be FormalContext;

      let CP1,CP2 be strict FormalConcept of C;

      

       A1: (the Extent of CP1 /\ the Extent of CP2) c= the Extent of CP2 by XBOOLE_1: 17;

      (( B-meet C) . (CP1,CP2)) in ( rng ( B-meet C)) by Lm2;

      then

      reconsider CP9 = (( B-meet C) . (CP1,CP2)) as strict FormalConcept of C by Th31;

      

       A2: (ex O be Subset of the carrier of C, A be 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 be Subset of the carrier of C, A9 be Subset of the carrier' of C st (( B-join C) . (CP9,CP2)) = ConceptStr (# O9, A9 #) & O9 = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP9 \/ the Extent of CP2))) & A9 = (the Intent of CP9 /\ the Intent of CP2) by Def17, Def18;

      (( AttributeDerivation C) . (( ObjectDerivation C) . ((the Extent of CP1 /\ the Extent of CP2) \/ the Extent of CP2))) = (( AttributeDerivation C) . ((( ObjectDerivation C) . (the Extent of CP1 /\ the Extent of CP2)) /\ (( ObjectDerivation C) . the Extent of CP2))) by Th15;

      

      then

       A3: (( AttributeDerivation C) . (( ObjectDerivation C) . ((the Extent of CP1 /\ the Extent of CP2) \/ the Extent of CP2))) = (( AttributeDerivation C) . (( ObjectDerivation C) . the Extent of CP2)) by A1, Th3, XBOOLE_1: 28

      .= (( AttributeDerivation C) . the Intent of CP2) by Def9

      .= the Extent of CP2 by Def9;

      ((( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP2))) /\ the Intent of CP2) = ((( ObjectDerivation C) . ((( AttributeDerivation C) . the Intent of CP1) /\ (( AttributeDerivation C) . the Intent of CP2))) /\ the Intent of CP2) by Th16

      .= ((( ObjectDerivation C) . (the Extent of CP1 /\ (( AttributeDerivation C) . the Intent of CP2))) /\ the Intent of CP2) by Def9

      .= ((( ObjectDerivation C) . (the Extent of CP1 /\ the Extent of CP2)) /\ the Intent of CP2) by Def9

      .= ((( ObjectDerivation C) . (the Extent of CP1 /\ the Extent of CP2)) /\ (( ObjectDerivation C) . the Extent of CP2)) by Def9

      .= (( ObjectDerivation C) . the Extent of CP2) by A1, Th3, XBOOLE_1: 28

      .= the Intent of CP2 by Def9;

      hence thesis by A2, A3;

    end;

    theorem :: CONLAT_1:37

    

     Th37: for C be FormalContext holds for CP1,CP2 be strict FormalConcept of C holds (( B-meet C) . (CP1,(( B-join C) . (CP1,CP2)))) = CP1

    proof

      let C be FormalContext;

      let CP1,CP2 be strict FormalConcept of C;

      

       A1: (the Intent of CP1 /\ the Intent of CP2) c= the Intent of CP1 by XBOOLE_1: 17;

      (( B-join C) . (CP1,CP2)) in ( rng ( B-join C)) by Lm3;

      then

      reconsider CP9 = (( B-join C) . (CP1,CP2)) as strict FormalConcept of C by Th31;

      

       A2: (ex O be Subset of the carrier of C, A be 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 be Subset of the carrier of C, A9 be Subset of the carrier' of C st (( B-meet C) . (CP1,CP9)) = ConceptStr (# O9, A9 #) & O9 = (the Extent of CP1 /\ the Extent of CP9) & A9 = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP9))) by Def17, Def18;

      (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ (the Intent of CP1 /\ the Intent of CP2)))) = (( ObjectDerivation C) . ((( AttributeDerivation C) . the Intent of CP1) /\ (( AttributeDerivation C) . (the Intent of CP1 /\ the Intent of CP2)))) by Th16;

      

      then

       A3: (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP1 \/ (the Intent of CP1 /\ the Intent of CP2)))) = (( ObjectDerivation C) . (( AttributeDerivation C) . the Intent of CP1)) by A1, Th4, XBOOLE_1: 28

      .= (( ObjectDerivation C) . the Extent of CP1) by Def9

      .= the Intent of CP1 by Def9;

      (the Extent of CP1 /\ (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)))) = (the Extent of CP1 /\ (( AttributeDerivation C) . ((( ObjectDerivation C) . the Extent of CP1) /\ (( ObjectDerivation C) . the Extent of CP2)))) by Th15

      .= (the Extent of CP1 /\ (( AttributeDerivation C) . (the Intent of CP1 /\ (( ObjectDerivation C) . the Extent of CP2)))) by Def9

      .= (the Extent of CP1 /\ (( AttributeDerivation C) . (the Intent of CP1 /\ the Intent of CP2))) by Def9

      .= ((( AttributeDerivation C) . the Intent of CP1) /\ (( AttributeDerivation C) . (the Intent of CP1 /\ the Intent of CP2))) by Def9

      .= (( AttributeDerivation C) . the Intent of CP1) by A1, Th4, XBOOLE_1: 28

      .= the Extent of CP1 by Def9;

      hence thesis by A2, A3;

    end;

    theorem :: CONLAT_1:38

    for C be FormalContext holds for CP be strict FormalConcept of C holds (( B-meet C) . (CP,( Concept-with-all-Objects C))) = CP

    proof

      let C be FormalContext;

      let CP be strict FormalConcept of C;

      consider O be Subset of the carrier of C, A be Subset of the carrier' of C such that

       A1: (( B-meet C) . (CP,( Concept-with-all-Objects C))) = ConceptStr (# O, A #) and

       A2: O = (the Extent of CP /\ the Extent of ( Concept-with-all-Objects C)) and

       A3: A = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP \/ the Intent of ( Concept-with-all-Objects C)))) by Def17;

      

       A4: O = (the Extent of CP /\ the carrier of C) by A2, Th23

      .= the Extent of CP by XBOOLE_1: 28;

      the carrier of C c= the carrier of C;

      then

      reconsider O9 = the carrier of C as Subset of the carrier of C;

      

       A5: ((( ObjectDerivation C) . the Extent of CP) \/ (( ObjectDerivation C) . O9)) = (( ObjectDerivation C) . the Extent of CP) by Th3, XBOOLE_1: 12;

      A = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP \/ (( ObjectDerivation C) . the Extent of ( Concept-with-all-Objects C))))) by A3, Def9

      .= (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP \/ (( ObjectDerivation C) . the carrier of C)))) by Th23

      .= (( ObjectDerivation C) . (( AttributeDerivation C) . (( ObjectDerivation C) . the Extent of CP))) by A5, Def9

      .= (( ObjectDerivation C) . the Extent of CP) by Th7

      .= the Intent of CP by Def9;

      hence thesis by A1, A4;

    end;

    theorem :: CONLAT_1:39

    

     Th39: for C be FormalContext holds for CP be strict FormalConcept of C holds (( B-join C) . (CP,( Concept-with-all-Objects C))) = ( Concept-with-all-Objects C)

    proof

      let C be FormalContext;

      let CP be strict FormalConcept of C;

      consider O be Subset of the carrier of C, A be Subset of the carrier' of C such that

       A1: (( B-join C) . (CP,( Concept-with-all-Objects C))) = ConceptStr (# O, A #) and

       A2: O = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP \/ the Extent of ( Concept-with-all-Objects C)))) and

       A3: A = (the Intent of CP /\ the Intent of ( Concept-with-all-Objects C)) by Def18;

      

       A4: O = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP \/ the carrier of C))) by A2, Th23

      .= (( AttributeDerivation C) . (( ObjectDerivation C) . the carrier of C)) by XBOOLE_1: 12

      .= (( AttributeDerivation C) . (( ObjectDerivation C) . the Extent of ( Concept-with-all-Objects C))) by Th23

      .= (( AttributeDerivation C) . the Intent of ( Concept-with-all-Objects C)) by Def9

      .= the Extent of ( Concept-with-all-Objects C) by Def9;

      A = ((( ObjectDerivation C) . the Extent of CP) /\ the Intent of ( Concept-with-all-Objects C)) by A3, Def9

      .= ((( ObjectDerivation C) . the Extent of CP) /\ (( ObjectDerivation C) . the Extent of ( Concept-with-all-Objects C))) by Def9

      .= (( ObjectDerivation C) . (the Extent of CP \/ the Extent of ( Concept-with-all-Objects C))) by Th15

      .= (( ObjectDerivation C) . (the Extent of CP \/ the carrier of C)) by Th23

      .= (( ObjectDerivation C) . the carrier of C) by XBOOLE_1: 12

      .= (( ObjectDerivation C) . the Extent of ( Concept-with-all-Objects C)) by Th23

      .= the Intent of ( Concept-with-all-Objects C) by Def9;

      hence thesis by A1, A4;

    end;

    theorem :: CONLAT_1:40

    for C be FormalContext holds for CP be strict FormalConcept of C holds (( B-join C) . (CP,( Concept-with-all-Attributes C))) = CP

    proof

      let C be FormalContext;

      let CP be strict FormalConcept of C;

      consider O be Subset of the carrier of C, A be Subset of the carrier' of C such that

       A1: (( B-join C) . (CP,( Concept-with-all-Attributes C))) = ConceptStr (# O, A #) and

       A2: O = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP \/ the Extent of ( Concept-with-all-Attributes C)))) and

       A3: A = (the Intent of CP /\ the Intent of ( Concept-with-all-Attributes C)) by Def18;

      

       A4: A = (the Intent of CP /\ the carrier' of C) by A3, Th23

      .= the Intent of CP by XBOOLE_1: 28;

      the carrier' of C c= the carrier' of C;

      then

      reconsider A9 = the carrier' of C as Subset of the carrier' of C;

      

       A5: ((( AttributeDerivation C) . the Intent of CP) \/ (( AttributeDerivation C) . A9)) = (( AttributeDerivation C) . the Intent of CP) by Th4, XBOOLE_1: 12;

      O = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP \/ (( AttributeDerivation C) . the Intent of ( Concept-with-all-Attributes C))))) by A2, Def9

      .= (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of CP \/ (( AttributeDerivation C) . the carrier' of C)))) by Th23

      .= (( AttributeDerivation C) . (( ObjectDerivation C) . (( AttributeDerivation C) . the Intent of CP))) by A5, Def9

      .= (( AttributeDerivation C) . the Intent of CP) by Th8

      .= the Extent of CP by Def9;

      hence thesis by A1, A4;

    end;

    theorem :: CONLAT_1:41

    for C be FormalContext holds for CP be strict FormalConcept of C holds (( B-meet C) . (CP,( Concept-with-all-Attributes C))) = ( Concept-with-all-Attributes C)

    proof

      let C be FormalContext;

      let CP be strict FormalConcept of C;

      consider O be Subset of the carrier of C, A be Subset of the carrier' of C such that

       A1: (( B-meet C) . (CP,( Concept-with-all-Attributes C))) = ConceptStr (# O, A #) and

       A2: O = (the Extent of CP /\ the Extent of ( Concept-with-all-Attributes C)) and

       A3: A = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP \/ the Intent of ( Concept-with-all-Attributes C)))) by Def17;

      

       A4: A = (( ObjectDerivation C) . (( AttributeDerivation C) . (the Intent of CP \/ the carrier' of C))) by A3, Th23

      .= (( ObjectDerivation C) . (( AttributeDerivation C) . the carrier' of C)) by XBOOLE_1: 12

      .= (( ObjectDerivation C) . (( AttributeDerivation C) . the Intent of ( Concept-with-all-Attributes C))) by Th23

      .= (( ObjectDerivation C) . the Extent of ( Concept-with-all-Attributes C)) by Def9

      .= the Intent of ( Concept-with-all-Attributes C) by Def9;

      O = ((( AttributeDerivation C) . the Intent of CP) /\ the Extent of ( Concept-with-all-Attributes C)) by A2, Def9

      .= ((( AttributeDerivation C) . the Intent of CP) /\ (( AttributeDerivation C) . the Intent of ( Concept-with-all-Attributes C))) by Def9

      .= (( AttributeDerivation C) . (the Intent of CP \/ the Intent of ( Concept-with-all-Attributes C))) by Th16

      .= (( AttributeDerivation C) . (the Intent of CP \/ the carrier' of C)) by Th23

      .= (( AttributeDerivation C) . the carrier' of C) by XBOOLE_1: 12

      .= (( AttributeDerivation C) . the Intent of ( Concept-with-all-Attributes C)) by Th23

      .= the Extent of ( Concept-with-all-Attributes C) by Def9;

      hence thesis by A1, A4;

    end;

    definition

      let C be FormalContext;

      :: CONLAT_1:def20

      func ConceptLattice (C) -> strict non empty LattStr equals LattStr (# ( B-carrier C), ( B-join C), ( B-meet C) #);

      coherence ;

    end

    theorem :: CONLAT_1:42

    

     Th42: for C be FormalContext holds ( ConceptLattice C) is Lattice

    proof

      let C be FormalContext;

      set L = LattStr (# ( B-carrier C), ( B-join C), ( B-meet C) #);

      reconsider L as strict non empty LattStr;

      

       A1: for a,b,c be Element of L holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c)

      proof

        let a,b,c be Element of L;

        reconsider b, c as Element of ( B-carrier C);

        reconsider d = (( B-join C) . (b,c)) as Element of L;

        reconsider b, c as Element of L;

        reconsider a, b as Element of ( B-carrier C);

        reconsider e = (( B-join C) . (a,b)) as Element of L;

        reconsider a, b as Element of L;

        

         A2: (a "\/" (b "\/" c)) = (a "\/" d) by LATTICES:def 1

        .= (( B-join C) . (a,(( B-join C) . (b,c)))) by LATTICES:def 1;

        

         A3: ((a "\/" b) "\/" c) = (e "\/" c) by LATTICES:def 1

        .= (( B-join C) . ((( B-join C) . (a,b)),c)) by LATTICES:def 1;

        reconsider a, b, c as strict FormalConcept of C by Th31;

        (( B-join C) . (a,(( B-join C) . (b,c)))) = (( B-join C) . ((( B-join C) . (a,b)),c)) by Th35;

        hence thesis by A2, A3;

      end;

      

       A4: for a,b be Element of L holds ((a "/\" b) "\/" b) = b

      proof

        let a,b be Element of L;

        reconsider a, b as Element of ( B-carrier C);

        reconsider d = (( B-meet C) . (a,b)) as Element of L;

        reconsider a, b as Element of L;

        

         A5: ((a "/\" b) "\/" b) = (d "\/" b) by LATTICES:def 2

        .= (( B-join C) . ((( B-meet C) . (a,b)),b)) by LATTICES:def 1;

        reconsider a, b as strict FormalConcept of C by Th31;

        (( B-join C) . ((( B-meet C) . (a,b)),b)) = b by Th36;

        hence thesis by A5;

      end;

      

       A6: for a,b,c be Element of L holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)

      proof

        let a,b,c be Element of L;

        reconsider b, c as Element of ( B-carrier C);

        reconsider d = (( B-meet C) . (b,c)) as Element of L;

        reconsider b, c as Element of L;

        

         A7: (a "/\" (b "/\" c)) = (a "/\" d) by LATTICES:def 2

        .= (( B-meet C) . (a,(( B-meet C) . (b,c)))) by LATTICES:def 2;

        reconsider a, b as Element of ( B-carrier C);

        reconsider e = (( B-meet C) . (a,b)) as Element of L;

        reconsider a, b as Element of L;

        

         A8: ((a "/\" b) "/\" c) = (e "/\" c) by LATTICES:def 2

        .= (( B-meet C) . ((( B-meet C) . (a,b)),c)) by LATTICES:def 2;

        reconsider a, b, c as strict FormalConcept of C by Th31;

        (( B-meet C) . (a,(( B-meet C) . (b,c)))) = (( B-meet C) . ((( B-meet C) . (a,b)),c)) by Th34;

        hence thesis by A7, A8;

      end;

      

       A9: for a,b be Element of L holds (a "/\" b) = (b "/\" a)

      proof

        let a,b be Element of L;

        

         A10: (b "/\" a) = (( B-meet C) . (b,a)) by LATTICES:def 2;

        reconsider a, b as strict FormalConcept of C by Th31;

        (( B-meet C) . (a,b)) = (( B-meet C) . (b,a)) by Th32;

        hence thesis by A10, LATTICES:def 2;

      end;

      

       A11: for a,b be Element of L holds (a "/\" (a "\/" b)) = a

      proof

        let a,b be Element of L;

        reconsider a, b as Element of ( B-carrier C);

        reconsider d = (( B-join C) . (a,b)) as Element of L;

        reconsider a, b as Element of L;

        

         A12: (a "/\" (a "\/" b)) = (a "/\" d) by LATTICES:def 1

        .= (( B-meet C) . (a,(( B-join C) . (a,b)))) by LATTICES:def 2;

        reconsider a, b as strict FormalConcept of C by Th31;

        (( B-meet C) . (a,(( B-join C) . (a,b)))) = a by Th37;

        hence thesis by A12;

      end;

      for a,b be Element of L holds (a "\/" b) = (b "\/" a)

      proof

        let a,b be Element of L;

        

         A13: (b "\/" a) = (( B-join C) . (b,a)) by LATTICES:def 1;

        reconsider a, b as strict FormalConcept of C by Th31;

        (( B-join C) . (a,b)) = (( B-join C) . (b,a)) by Th33;

        hence thesis by A13, LATTICES:def 1;

      end;

      then L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A1, A4, A9, A6, A11, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;

      hence thesis;

    end;

    registration

      let C be FormalContext;

      cluster ( ConceptLattice C) -> strict non empty Lattice-like;

      coherence by Th42;

    end

    definition

      let C be FormalContext;

      let S be non empty Subset of ( ConceptLattice C);

      :: original: Element

      redefine

      mode Element of S -> FormalConcept of C ;

      coherence

      proof

        let s be Element of S;

        s is Element of ( B-carrier C);

        hence thesis;

      end;

    end

    definition

      let C be FormalContext;

      let CP be Element of ( ConceptLattice C);

      :: CONLAT_1:def21

      func CP @ -> strict FormalConcept of C equals CP;

      coherence by Th31;

    end

    theorem :: CONLAT_1:43

    

     Th43: for C be FormalContext holds for CP1,CP2 be Element of ( ConceptLattice C) holds CP1 [= CP2 iff (CP1 @ ) is-SubConcept-of (CP2 @ )

    proof

      let C be FormalContext;

      let CP1,CP2 be Element of ( ConceptLattice C);

      set CL = ( ConceptLattice C);

       A1:

      now

        assume

         A2: (CP1 @ ) is-SubConcept-of (CP2 @ );

        then the Intent of (CP2 @ ) c= the Intent of (CP1 @ ) by Th28;

        then

         A3: (the Intent of (CP1 @ ) /\ the Intent of (CP2 @ )) = the Intent of (CP2 @ ) by XBOOLE_1: 28;

        consider O be Subset of the carrier of C, A be Subset of the carrier' of C such that

         A4: (( B-join C) . ((CP1 @ ),(CP2 @ ))) = ConceptStr (# O, A #) and

         A5: O = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of (CP1 @ ) \/ the Extent of (CP2 @ )))) and

         A6: A = (the Intent of (CP1 @ ) /\ the Intent of (CP2 @ )) by Def18;

        the Extent of (CP1 @ ) c= the Extent of (CP2 @ ) by A2;

        then (the Extent of (CP1 @ ) \/ the Extent of (CP2 @ )) = the Extent of (CP2 @ ) by XBOOLE_1: 12;

        

        then O = (( AttributeDerivation C) . the Intent of (CP2 @ )) by A5, Def9

        .= the Extent of (CP2 @ ) by Def9;

        then (CP1 "\/" CP2) = CP2 by A3, A4, A6, LATTICES:def 1;

        hence CP1 [= CP2 by LATTICES:def 3;

      end;

      now

        assume CP1 [= CP2;

        then (CP1 "\/" CP2) = CP2 by LATTICES:def 3;

        then

         A7: (the L_join of CL . (CP1,CP2)) = CP2 by LATTICES:def 1;

        ex O be Subset of the carrier of C, A be Subset of the carrier' of C st (( B-join C) . ((CP1 @ ),(CP2 @ ))) = ConceptStr (# O, A #) & O = (( AttributeDerivation C) . (( ObjectDerivation C) . (the Extent of (CP1 @ ) \/ the Extent of (CP2 @ )))) & A = (the Intent of (CP1 @ ) /\ the Intent of (CP2 @ )) by Def18;

        then for x be object holds x in the Intent of (CP2 @ ) implies x in the Intent of (CP1 @ ) by A7, XBOOLE_0:def 4;

        then the Intent of (CP2 @ ) c= the Intent of (CP1 @ );

        hence (CP1 @ ) is-SubConcept-of (CP2 @ ) by Th28;

      end;

      hence thesis by A1;

    end;

    theorem :: CONLAT_1:44

    

     Th44: for C be FormalContext holds ( ConceptLattice C) is complete Lattice

    proof

      let C be FormalContext;

      for X be Subset of ( ConceptLattice C) holds ex a be Element of ( ConceptLattice C) st a is_less_than X & for b be Element of ( ConceptLattice C) st b is_less_than X holds b [= a

      proof

        let X be Subset of ( ConceptLattice C);

        per cases ;

          suppose

           A1: X = {} ;

          

           A2: for b be Element of ( ConceptLattice C) st b is_less_than X holds b [= ( Top ( ConceptLattice C))

          proof

            let b be Element of ( ConceptLattice C);

            assume b is_less_than X;

            ex c be Element of ( ConceptLattice C) st for a be 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 be Element of ( ConceptLattice C) holds (CO "\/" CP) = CO & (CP "\/" CO) = CO

              proof

                let CP be Element of ( ConceptLattice C);

                reconsider CP as strict FormalConcept of C by Th31;

                reconsider CO as strict FormalConcept of C;

                (( B-join C) . (CO,CP)) = (( B-join C) . (CP,CO)) by Th33

                .= CO by Th39;

                hence thesis by LATTICES:def 1;

              end;

              hence thesis;

            end;

            then ( ConceptLattice C) is upper-bounded by LATTICES:def 14;

            then (( Top ( ConceptLattice C)) "\/" b) = ( Top ( ConceptLattice C));

            hence thesis by LATTICES:def 3;

          end;

          for q be Element of ( ConceptLattice C) st q in X holds ( Top ( ConceptLattice C)) [= q by A1;

          then ( Top ( ConceptLattice C)) is_less_than X by LATTICE3:def 16;

          hence thesis by A2;

        end;

          suppose X <> {} ;

          then

          reconsider X as non empty Subset of ( ConceptLattice C);

          set ExX = { the Extent of x where x be Element of ( B-carrier C) : x in X };

          

           A3: for x be Element of X holds the Extent of x in ExX

          proof

            let x be Element of X;

            x in X;

            then

            reconsider x as Element of ( B-carrier C);

            the Extent of x in ExX;

            hence thesis;

          end;

          then

          reconsider ExX as non empty set;

          set E1 = ( meet ExX);

          

           A4: for o be Object of C holds o in E1 iff for x be Element of X holds o in the Extent of x

          proof

            let o be Object of C;

            

             A5: (for x be Element of X holds o in the Extent of x) implies o in E1

            proof

              assume

               A6: for x be Element of X holds o in the Extent of x;

              for Y be set holds Y in ExX implies o in Y

              proof

                let Y be set;

                assume Y in ExX;

                then ex Y9 be Element of ( B-carrier C) st Y = the Extent of Y9 & Y9 in X;

                hence thesis by A6;

              end;

              hence thesis by SETFAM_1:def 1;

            end;

            o in E1 implies for x be Element of X holds o in the Extent of x

            proof

              assume

               A7: o in E1;

              let x be Element of X;

              the Extent of x in ExX by A3;

              hence thesis by A7, SETFAM_1:def 1;

            end;

            hence thesis by A5;

          end;

          E1 c= the carrier of C

          proof

            set Y = the Element of ExX;

            let x be object;

            Y in ExX;

            then

            consider Y9 be Element of ( B-carrier C) such that

             A8: Y = the Extent of Y9 and Y9 in X;

            assume x in E1;

            then x in the Extent of Y9 by A8, SETFAM_1:def 1;

            hence thesis;

          end;

          then

          consider O be Subset of the carrier of C such that

           A9: for o be Object of C holds o in O iff for x be Element of X holds o in the Extent of x by A4;

          set InX = { the Intent of x where x be Element of ( B-carrier C) : x in X };

          set In = ( union InX);

          

           A10: for a be Attribute of C holds a in In iff ex x be Element of X st a in the Intent of x

          proof

            let a be Attribute of C;

            

             A11: (ex x be Element of X st a in the Intent of x) implies a in In

            proof

              assume

               A12: ex x be Element of X st a in the Intent of x;

              ex Y be set st a in Y & Y in InX

              proof

                consider x be Element of X such that

                 A13: a in the Intent of x by A12;

                x in X;

                then the Intent of x in InX;

                hence thesis by A13;

              end;

              hence thesis by TARSKI:def 4;

            end;

            a in In implies ex x be Element of X st a in the Intent of x

            proof

              assume a in In;

              then

              consider Y be set such that

               A14: a in Y and

               A15: Y in InX by TARSKI:def 4;

              ex Y9 be Element of ( B-carrier C) st Y = the Intent of Y9 & Y9 in X by A15;

              hence thesis by A14;

            end;

            hence thesis by A11;

          end;

          In c= the carrier' of C

          proof

            let x be object;

            assume x in In;

            then

            consider Y be set such that

             A16: x in Y and

             A17: Y in InX by TARSKI:def 4;

            ex Y9 be Element of ( B-carrier C) st Y = the Intent of Y9 & Y9 in X by A17;

            hence thesis by A16;

          end;

          then

          consider A9 be Subset of the carrier' of C such that

           A18: for a be Attribute of C holds a in A9 iff ex x be Element of X st a in the Intent of x by A10;

          

           A19: for o be Object of C holds o in O iff for x be Element of X holds o in (( AttributeDerivation C) . the Intent of x)

          proof

            let o be Object of C;

            

             A20: (for x be Element of X holds o in (( AttributeDerivation C) . the Intent of x)) implies o in O

            proof

              assume

               A21: for x be Element of X holds o in (( AttributeDerivation C) . the Intent of x);

              for x be Element of X holds o in the Extent of x

              proof

                let x be Element of X;

                o in (( AttributeDerivation C) . the Intent of x) by A21;

                hence thesis by Def9;

              end;

              hence thesis by A9;

            end;

            o in O implies for x be Element of X holds o in (( AttributeDerivation C) . the Intent of x)

            proof

              assume

               A22: o in O;

              for x be Element of X holds o in (( AttributeDerivation C) . the Intent of x)

              proof

                let x be Element of X;

                o in the Extent of x by A9, A22;

                hence thesis by Def9;

              end;

              hence thesis;

            end;

            hence thesis by A20;

          end;

          

           A23: for x be object holds x in (( AttributeDerivation C) . A9) implies x in O

          proof

            let x be object;

            assume x in (( AttributeDerivation C) . A9);

            then x in { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a } by Def3;

            then

            consider x9 be Object of C such that

             A24: x9 = x and

             A25: for a be Attribute of C st a in A9 holds x9 is-connected-with a;

            for x be Element of X holds x9 in (( AttributeDerivation C) . the Intent of x)

            proof

              let x be Element of X;

              for a be Attribute of C st a in the Intent of x holds x9 is-connected-with a by A18, A25;

              then x9 in { o where o be Object of C : for a be Attribute of C st a in the Intent of x holds o is-connected-with a };

              hence thesis by Def3;

            end;

            hence thesis by A19, A24;

          end;

          consider A be Subset of the carrier' of C such that

           A26: A = (( ObjectDerivation C) . (( AttributeDerivation C) . A9));

          set p = ConceptStr (# O, A #);

          for x be object holds x in O implies x in (( AttributeDerivation C) . A9)

          proof

            let x9 be object;

            assume

             A27: x9 in O;

            then

            reconsider x9 as Object of C;

            for a be Attribute of C st a in A9 holds x9 is-connected-with a

            proof

              let a be Attribute of C;

              assume a in A9;

              then

              consider x be 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 be Object of C : for a be Attribute of C st a in the Intent of x holds o is-connected-with a } by Def3;

              then ex y be Object of C st y = x9 & for a be Attribute of C st a in the Intent of x holds y is-connected-with a;

              hence thesis by A28;

            end;

            then x9 in { o where o be Object of C : for a be Attribute of C st a in A9 holds o is-connected-with a };

            hence thesis by Def3;

          end;

          then O = (( AttributeDerivation C) . A9) by A23, TARSKI: 2;

          then p is FormalConcept of C by A26, Th21;

          then

          reconsider p as Element of ( ConceptLattice C) by Th31;

          

           A29: for b be Element of ( ConceptLattice C) st b is_less_than X holds b [= p

          proof

            let b be Element of ( ConceptLattice C);

            assume

             A30: b is_less_than X;

            the Extent of (b @ ) c= the Extent of (p @ )

            proof

              let x9 be object;

              assume

               A31: x9 in the Extent of (b @ );

              then

              reconsider x9 as Object of C;

              for x be Element of X holds x9 in the Extent of x

              proof

                let x be Element of X;

                x in X;

                then

                reconsider x as Element of ( ConceptLattice C);

                b [= x by A30, LATTICE3:def 16;

                then (b @ ) is-SubConcept-of (x @ ) by Th43;

                then the Extent of (b @ ) c= the Extent of (x @ );

                hence thesis by A31;

              end;

              hence thesis by A9;

            end;

            then (b @ ) is-SubConcept-of (p @ );

            hence thesis by Th43;

          end;

          for q be Element of ( ConceptLattice C) st q in X holds p [= q

          proof

            let q be Element of ( ConceptLattice C);

            assume

             A32: q in X;

            the Extent of (p @ ) c= the Extent of (q @ ) by A9, A32;

            then (p @ ) is-SubConcept-of (q @ );

            hence thesis by Th43;

          end;

          then p is_less_than X by LATTICE3:def 16;

          hence thesis by A29;

        end;

      end;

      hence thesis by VECTSP_8:def 6;

    end;

    registration

      let C be FormalContext;

      cluster ( ConceptLattice C) -> complete;

      coherence by Th44;

    end