substlat.miz



    begin

    reserve V,C for set;

    definition

      let V, C;

      :: SUBSTLAT:def1

      func SubstitutionSet (V,C) -> Subset of ( Fin ( PFuncs (V,C))) equals { A where A be Element of ( Fin ( PFuncs (V,C))) : (for u be set st u in A holds u is finite) & for s,t be Element of ( PFuncs (V,C)) holds (s in A & t in A & s c= t implies s = t) };

      coherence

      proof

        set IT = { A where A be Element of ( Fin ( PFuncs (V,C))) : (for u be set st u in A holds u is finite) & for s,t be Element of ( PFuncs (V,C)) holds (s in A & t in A & s c= t implies s = t) };

        IT c= ( Fin ( PFuncs (V,C)))

        proof

          let x be object;

          assume x in IT;

          then ex B be Element of ( Fin ( PFuncs (V,C))) st B = x & (for u be set st u in B holds u is finite) & for s,t be Element of ( PFuncs (V,C)) holds (s in B & t in B & s c= t implies s = t);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    

     Lm1: for a,b be set st b in ( SubstitutionSet (V,C)) & a in b holds a is finite

    proof

      let a,b be set;

      assume that

       A1: b in ( SubstitutionSet (V,C)) and

       A2: a in b;

      ex A be Element of ( Fin ( PFuncs (V,C))) st A = b & (for u be set st u in A holds u is finite) & for s,t be Element of ( PFuncs (V,C)) holds (s in A & t in A & s c= t implies s = t) by A1;

      hence thesis by A2;

    end;

    theorem :: SUBSTLAT:1

    

     Th1: {} in ( SubstitutionSet (V,C))

    proof

       {} c= ( PFuncs (V,C));

      then

       A1: {} in ( Fin ( PFuncs (V,C))) by FINSUB_1:def 5;

      (for u be set st u in {} holds u is finite) & for s,t be Element of ( PFuncs (V,C)) holds (s in {} & t in {} & s c= t implies s = t);

      hence thesis by A1;

    end;

    theorem :: SUBSTLAT:2

    

     Th2: { {} } in ( SubstitutionSet (V,C))

    proof

      

       A1: for s,t be Element of ( PFuncs (V,C)) holds (s in { {} } & t in { {} } & s c= t implies s = t)

      proof

        let s,t be Element of ( PFuncs (V,C));

        assume that

         A2: s in { {} } and

         A3: t in { {} } and s c= t;

        s = {} by A2, TARSKI:def 1;

        hence thesis by A3, TARSKI:def 1;

      end;

       {} is PartFunc of V, C by RELSET_1: 12;

      then {} in ( PFuncs (V,C)) by PARTFUN1: 45;

      then { {} } c= ( PFuncs (V,C)) by ZFMISC_1: 31;

      then

       A4: { {} } in ( Fin ( PFuncs (V,C))) by FINSUB_1:def 5;

      for u be set st u in { {} } holds u is finite;

      hence thesis by A4, A1;

    end;

    registration

      let V, C;

      cluster ( SubstitutionSet (V,C)) -> non empty;

      coherence by Th2;

    end

    definition

      let V, C;

      let A,B be Element of ( SubstitutionSet (V,C));

      :: original: \/

      redefine

      func A \/ B -> Element of ( Fin ( PFuncs (V,C))) ;

      coherence

      proof

        (A \/ B) in ( Fin ( PFuncs (V,C)));

        hence thesis;

      end;

    end

    registration

      let V, C;

      cluster non empty for Element of ( SubstitutionSet (V,C));

      existence

      proof

         { {} } in ( SubstitutionSet (V,C)) by Th2;

        hence thesis;

      end;

    end

    registration

      let V, C;

      cluster -> finite for Element of ( SubstitutionSet (V,C));

      coherence ;

    end

    definition

      let V, C;

      let A be Element of ( Fin ( PFuncs (V,C)));

      :: SUBSTLAT:def2

      func mi A -> Element of ( SubstitutionSet (V,C)) equals { t where t be Element of ( PFuncs (V,C)) : t is finite & for s be Element of ( PFuncs (V,C)) holds (s in A & s c= t iff s = t) };

      coherence

      proof

        set M = { t where t be Element of ( PFuncs (V,C)) : t is finite & for s be Element of ( PFuncs (V,C)) holds (s in A & s c= t iff s = t) };

        

         A1: M c= ( PFuncs (V,C))

        proof

          let a be object;

          assume a in M;

          then ex t9 be Element of ( PFuncs (V,C)) st a = t9 & t9 is finite & for s be Element of ( PFuncs (V,C)) holds (s in A & s c= t9 iff s = t9);

          hence thesis;

        end;

         A2:

        now

          let x be object;

          assume x in M;

          then ex t be Element of ( PFuncs (V,C)) st x = t & t is finite & for s be Element of ( PFuncs (V,C)) holds s in A & s c= t iff s = t;

          hence x in A;

        end;

        then

         A3: M c= A;

        reconsider M as set;

        reconsider M9 = M as Element of ( Fin ( PFuncs (V,C))) by A1, A3, FINSUB_1:def 5;

        

         A4: for u be set st u in M9 holds u is finite

        proof

          let u be set;

          assume u in M9;

          then ex t9 be Element of ( PFuncs (V,C)) st u = t9 & t9 is finite & for s be Element of ( PFuncs (V,C)) holds (s in A & s c= t9 iff s = t9);

          hence thesis;

        end;

        for s,t be Element of ( PFuncs (V,C)) holds (s in M9 & t in M9 & s c= t implies s = t)

        proof

          let s,t be Element of ( PFuncs (V,C));

          assume that

           A5: s in M9 & t in M9 and

           A6: s c= t;

          s in A & ex tt be Element of ( PFuncs (V,C)) st t = tt & tt is finite & for ss be Element of ( PFuncs (V,C)) holds (ss in A & ss c= tt iff ss = tt) by A2, A5;

          hence thesis by A6;

        end;

        then M in { A1 where A1 be Element of ( Fin ( PFuncs (V,C))) : (for u be set st u in A1 holds u is finite) & for s,t be Element of ( PFuncs (V,C)) holds (s in A1 & t in A1 & s c= t implies s = t) } by A4;

        hence thesis;

      end;

    end

    registration

      let V, C;

      cluster -> functional for Element of ( SubstitutionSet (V,C));

      coherence

      proof

        let A be Element of ( SubstitutionSet (V,C));

        A c= ( PFuncs (V,C)) by FINSUB_1:def 5;

        hence thesis;

      end;

    end

    definition

      let V, C;

      let A,B be Element of ( Fin ( PFuncs (V,C)));

      :: SUBSTLAT:def3

      func A ^ B -> Element of ( Fin ( PFuncs (V,C))) equals { (s \/ t) where s,t be Element of ( PFuncs (V,C)) : s in A & t in B & s tolerates t };

      coherence

      proof

        deffunc U( Element of ( PFuncs (V,C)), Element of ( PFuncs (V,C))) = ($1 \/ $2);

        set M = { U(s,t) where s,t be Element of ( PFuncs (V,C)) : s in A & t in B & s tolerates t }, N = { U(s,t) where s,t be Element of ( PFuncs (V,C)) : s in A & t in B };

        

         A1: M c= N

        proof

          let a be object;

          assume a in M;

          then ex s,t be Element of ( PFuncs (V,C)) st a = (s \/ t) & s in A & t in B & s tolerates t;

          hence thesis;

        end;

        

         A2: M c= ( PFuncs (V,C))

        proof

          let y be object;

          assume y in M;

          then

          consider s,t be Element of ( PFuncs (V,C)) such that

           A3: y = (s \/ t) and s in A and t in B and

           A4: s tolerates t;

          reconsider s99 = s, t99 = t as PartFunc of V, C by PARTFUN1: 47;

          reconsider s9 = s, t9 = t as Function;

          s is PartFunc of V, C & t is PartFunc of V, C by PARTFUN1: 47;

          then (s9 +* t9) is PartFunc of V, C by FUNCT_4: 40;

          then (s99 \/ t99) is PartFunc of V, C by A4, FUNCT_4: 30;

          hence thesis by A3, PARTFUN1: 45;

        end;

        

         A5: B is finite;

        

         A6: A is finite;

        N is finite from FRAENKEL:sch 22( A6, A5);

        hence thesis by A1, A2, FINSUB_1:def 5;

      end;

    end

    reserve A,B,D for Element of ( Fin ( PFuncs (V,C)));

    theorem :: SUBSTLAT:3

    

     Th3: (A ^ B) = (B ^ A)

    proof

      deffunc U( Element of ( PFuncs (V,C)), Element of ( PFuncs (V,C))) = ($1 \/ $2);

      defpred X[ Function, Function] means $1 in A & $2 in B & $1 tolerates $2;

      defpred Y[ Function, Function] means $2 in B & $1 in A & $2 tolerates $1;

      set X1 = { U(s,t) where s be Element of ( PFuncs (V,C)), t be Element of ( PFuncs (V,C)) : X[s, t] };

      set X2 = { U(t,s) where s be Element of ( PFuncs (V,C)), t be Element of ( PFuncs (V,C)) : Y[s, t] };

       A1:

      now

        let x be object;

        x in X2 iff ex s,t be Element of ( PFuncs (V,C)) st x = U(t,s) & Y[s, t];

        then x in X2 iff ex t,s be Element of ( PFuncs (V,C)) st x = (t \/ s) & t in B & s in A & t tolerates s;

        hence x in X2 iff x in { (t \/ s) where t be Element of ( PFuncs (V,C)), s be Element of ( PFuncs (V,C)) : t in B & s in A & t tolerates s };

      end;

      

       A2: for s,t be Element of ( PFuncs (V,C)) holds U(s,t) = U(t,s);

      

       A3: for s,t be Element of ( PFuncs (V,C)) holds X[s, t] iff Y[s, t];

      X1 = X2 from FRAENKEL:sch 8( A3, A2);

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: SUBSTLAT:4

    

     Th4: B = { {} } implies (A ^ B) = A

    proof

      

       A1: { (s \/ t) where s,t be Element of ( PFuncs (V,C)) : s in A & t in { {} } & s tolerates t } c= A

      proof

        let a be object;

        assume a in { (s \/ t) where s,t be Element of ( PFuncs (V,C)) : s in A & t in { {} } & s tolerates t };

        then

        consider s9,t9 be Element of ( PFuncs (V,C)) such that

         A2: a = (s9 \/ t9) & s9 in A and

         A3: t9 in { {} } and s9 tolerates t9;

        t9 = {} by A3, TARSKI:def 1;

        hence thesis by A2;

      end;

      

       A4: A c= { (s \/ t) where s,t be Element of ( PFuncs (V,C)) : s in A & t in { {} } & s tolerates t }

      proof

         {} is PartFunc of V, C by RELSET_1: 12;

        then

        reconsider b = {} as Element of ( PFuncs (V,C)) by PARTFUN1: 45;

        let a be object;

        assume

         A5: a in A;

        A c= ( PFuncs (V,C)) by FINSUB_1:def 5;

        then

        reconsider a9 = a as Element of ( PFuncs (V,C)) by A5;

        

         A6: b in { {} } by TARSKI:def 1;

        a = (a9 \/ b) & a9 tolerates b by PARTFUN1: 59;

        hence thesis by A5, A6;

      end;

      assume B = { {} };

      hence thesis by A1, A4;

    end;

    theorem :: SUBSTLAT:5

    

     Th5: for a,b be set holds B in ( SubstitutionSet (V,C)) & a in B & b in B & a c= b implies a = b

    proof

      let a,b be set;

      assume B in ( SubstitutionSet (V,C));

      then

       A1: ex A1 be Element of ( Fin ( PFuncs (V,C))) st A1 = B & (for u be set st u in A1 holds u is finite) & for s,t be Element of ( PFuncs (V,C)) holds (s in A1 & t in A1 & s c= t implies s = t);

      assume that

       A2: a in B & b in B and

       A3: a c= b;

      B c= ( PFuncs (V,C)) by FINSUB_1:def 5;

      then

      reconsider a9 = a, b9 = b as Element of ( PFuncs (V,C)) by A2;

      a9 = b9 by A1, A2, A3;

      hence thesis;

    end;

    theorem :: SUBSTLAT:6

    

     Th6: for a be set holds a in ( mi B) implies a in B & for b be set holds b in B & b c= a implies b = a

    proof

      let a be set;

      assume a in ( mi B);

      then

       A1: ex t be Element of ( PFuncs (V,C)) st a = t & t is finite & for s be Element of ( PFuncs (V,C)) holds s in B & s c= t iff s = t;

      hence a in B;

      let b be set;

      assume that

       A2: b in B and

       A3: b c= a;

      B c= ( PFuncs (V,C)) by FINSUB_1:def 5;

      then

      reconsider b9 = b as Element of ( PFuncs (V,C)) by A2;

      b9 = a by A1, A2, A3;

      hence thesis;

    end;

    reserve s for Element of ( PFuncs (V,C));

    registration

      let V, C;

      cluster finite for Element of ( PFuncs (V,C));

      existence

      proof

         {} is PartFunc of V, C by RELSET_1: 12;

        then

        reconsider e = {} as Element of ( PFuncs (V,C)) by PARTFUN1: 45;

        take e;

        thus thesis;

      end;

    end

    theorem :: SUBSTLAT:7

    

     Th7: for a be finite set holds a in B & (for b be finite set st b in B & b c= a holds b = a) implies a in ( mi B)

    proof

      let a be finite set;

      assume that

       A1: a in B and

       A2: for s be finite set st s in B & s c= a holds s = a;

      B c= ( PFuncs (V,C)) by FINSUB_1:def 5;

      then

      reconsider a9 = a as Element of ( PFuncs (V,C)) by A1;

      s in B & s c= a iff s = a by A1, A2;

      then a9 in { t where t be Element of ( PFuncs (V,C)) : t is finite & for s be Element of ( PFuncs (V,C)) holds s in B & s c= t iff s = t };

      hence thesis;

    end;

    theorem :: SUBSTLAT:8

    

     Th8: ( mi A) c= A by Th6;

    theorem :: SUBSTLAT:9

    A = {} implies ( mi A) = {} by Th8, XBOOLE_1: 3;

    theorem :: SUBSTLAT:10

    

     Th10: for b be finite set holds b in B implies ex c be set st c c= b & c in ( mi B)

    proof

      defpred X[ set, set] means $1 c= $2;

      let b be finite set;

      assume

       A1: b in B;

      

       A2: B c= ( PFuncs (V,C)) by FINSUB_1:def 5;

      then

      reconsider b9 = b as Element of ( PFuncs (V,C)) by A1;

      

       A3: for a,b,c be Element of ( PFuncs (V,C)) st X[a, b] & X[b, c] holds X[a, c] by XBOOLE_1: 1;

      

       A4: for a be Element of ( PFuncs (V,C)) holds X[a, a];

      for a be Element of ( PFuncs (V,C)) st a in B holds ex b be Element of ( PFuncs (V,C)) st b in B & X[b, a] & for c be Element of ( PFuncs (V,C)) st c in B & X[c, b] holds X[b, c] from FRAENKEL:sch 23( A4, A3);

      then

      consider c be Element of ( PFuncs (V,C)) such that

       A5: c in B and

       A6: c c= b9 and

       A7: for a be Element of ( PFuncs (V,C)) st a in B & a c= c holds c c= a by A1;

      take c;

      thus c c= b by A6;

      for b be finite set st b in B & b c= c holds b = c by A2, A7;

      hence thesis by A5, A6, Th7;

    end;

    theorem :: SUBSTLAT:11

    

     Th11: for K be Element of ( SubstitutionSet (V,C)) holds ( mi K) = K

    proof

      let K be Element of ( SubstitutionSet (V,C));

      thus ( mi K) c= K by Th8;

      now

        let a be set;

        assume

         A1: a in K;

        then a is finite & for b be finite set st b in K & b c= a holds b = a by Lm1, Th5;

        hence a in ( mi K) by A1, Th7;

      end;

      hence thesis;

    end;

    theorem :: SUBSTLAT:12

    

     Th12: ( mi (A \/ B)) c= (( mi A) \/ B)

    proof

      now

        let a be set;

        assume

         A1: a in ( mi (A \/ B));

        then

        reconsider a9 = a as finite set by Lm1;

        

         A2: a in (A \/ B) by A1, Th6;

        now

          per cases by A2, XBOOLE_0:def 3;

            suppose

             A3: a in A;

            now

              let b be finite set;

              assume b in A;

              then b in (A \/ B) by XBOOLE_0:def 3;

              hence b c= a implies b = a by A1, Th6;

            end;

            then a9 in ( mi A) by A3, Th7;

            hence a in (( mi A) \/ B) by XBOOLE_0:def 3;

          end;

            suppose a in B;

            hence a in (( mi A) \/ B) by XBOOLE_0:def 3;

          end;

        end;

        hence a in (( mi A) \/ B);

      end;

      hence thesis;

    end;

    theorem :: SUBSTLAT:13

    

     Th13: ( mi (( mi A) \/ B)) = ( mi (A \/ B))

    proof

      

       A1: (( mi A) \/ B) c= (A \/ B) by Th8, XBOOLE_1: 9;

      now

        let a be set;

        assume

         A2: a in ( mi (( mi A) \/ B));

        then

        reconsider a9 = a as finite set by Lm1;

         A3:

        now

          let b be finite set;

          assume that

           A4: b in (A \/ B) and

           A5: b c= a;

          now

            per cases by A4, XBOOLE_0:def 3;

              suppose b in A;

              then

              consider c be set such that

               A6: c c= b and

               A7: c in ( mi A) by Th10;

              c in (( mi A) \/ B) & c c= a by A5, A6, A7, XBOOLE_0:def 3;

              then c = a by A2, Th6;

              hence b = a by A5, A6;

            end;

              suppose b in B;

              then b in (( mi A) \/ B) by XBOOLE_0:def 3;

              hence b = a by A2, A5, Th6;

            end;

          end;

          hence b = a;

        end;

        a in (( mi A) \/ B) by A2, Th6;

        then a9 in ( mi (A \/ B)) by A1, A3, Th7;

        hence a in ( mi (A \/ B));

      end;

      hence ( mi (( mi A) \/ B)) c= ( mi (A \/ B));

      

       A8: ( mi (A \/ B)) c= (( mi A) \/ B) by Th12;

      now

        let a be set;

        assume

         A9: a in ( mi (A \/ B));

        then

        reconsider a9 = a as finite set by Lm1;

        for b be finite set st b in (( mi A) \/ B) holds b c= a implies b = a by A1, A9, Th6;

        then a9 in ( mi (( mi A) \/ B)) by A8, A9, Th7;

        hence a in ( mi (( mi A) \/ B));

      end;

      hence thesis;

    end;

    theorem :: SUBSTLAT:14

    

     Th14: A c= B implies (A ^ D) c= (B ^ D)

    proof

      deffunc U( Element of ( PFuncs (V,C)), Element of ( PFuncs (V,C))) = ($1 \/ $2);

      defpred X[ Function, Function] means $1 in A & $2 in D & $1 tolerates $2;

      defpred Y[ Function, Function] means $1 in B & $2 in D & $1 tolerates $2;

      set X1 = { U(s,t) where s,t be Element of ( PFuncs (V,C)) : X[s, t] }, X2 = { U(s,t) where s,t be Element of ( PFuncs (V,C)) : Y[s, t] };

      assume A c= B;

      then

       A1: for s,t be Element of ( PFuncs (V,C)) holds X[s, t] implies Y[s, t];

      X1 c= X2 from FRAENKEL:sch 2( A1);

      hence thesis;

    end;

    theorem :: SUBSTLAT:15

    

     Th15: for a be set holds a in (A ^ B) implies ex b,c be set st b in A & c in B & a = (b \/ c)

    proof

      let a be set;

      assume a in (A ^ B);

      then ex s,t be Element of ( PFuncs (V,C)) st a = (s \/ t) & s in A & t in B & s tolerates t;

      hence thesis;

    end;

    theorem :: SUBSTLAT:16

    for b,c be Element of ( PFuncs (V,C)) holds b in A & c in B & b tolerates c implies (b \/ c) in (A ^ B);

    

     Lm2: for a be finite set holds a in (A ^ B) implies ex b be finite set st b c= a & b in (( mi A) ^ B)

    proof

      let a be finite set;

      assume a in (A ^ B);

      then

      consider b,c be Element of ( PFuncs (V,C)) such that

       A1: a = (b \/ c) and

       A2: b in A and

       A3: c in B and

       A4: b tolerates c;

      b is finite by A1, FINSET_1: 1, XBOOLE_1: 7;

      then

      consider d be set such that

       A5: d c= b and

       A6: d in ( mi A) by A2, Th10;

      

       A7: ( mi A) c= ( PFuncs (V,C)) by FINSUB_1:def 5;

      then

      reconsider d9 = d, c9 = c as Element of ( PFuncs (V,C)) by A6;

      reconsider d1 = d, b1 = b, c1 = c as PartFunc of V, C by A6, A7, PARTFUN1: 46;

      d1 c= b1 by A5;

      then

       A8: d9 tolerates c9 by A4, PARTFUN1: 58;

      then (d9 \/ c9) = (d9 +* c9) by FUNCT_4: 30;

      then

      reconsider e = (d1 \/ c1) as Element of ( PFuncs (V,C)) by PARTFUN1: 45;

      reconsider e as finite set by A1, A5, FINSET_1: 1, XBOOLE_1: 9;

      take e;

      thus e c= a by A1, A5, XBOOLE_1: 9;

      thus thesis by A3, A6, A8;

    end;

    theorem :: SUBSTLAT:17

    

     Th17: ( mi (A ^ B)) c= (( mi A) ^ B)

    proof

      

       A1: (( mi A) ^ B) c= (A ^ B) by Th8, Th14;

      now

        let a be set;

        assume

         A2: a in ( mi (A ^ B));

        then a in (A ^ B) & a is finite by Lm1, Th6;

        then ex b be finite set st b c= a & b in (( mi A) ^ B) by Lm2;

        hence a in (( mi A) ^ B) by A1, A2, Th6;

      end;

      hence thesis;

    end;

    theorem :: SUBSTLAT:18

    

     Th18: A c= B implies (D ^ A) c= (D ^ B)

    proof

      (D ^ A) = (A ^ D) & (D ^ B) = (B ^ D) by Th3;

      hence thesis by Th14;

    end;

    theorem :: SUBSTLAT:19

    

     Th19: ( mi (( mi A) ^ B)) = ( mi (A ^ B))

    proof

      

       A1: (( mi A) ^ B) c= (A ^ B) by Th8, Th14;

      now

        let a be set;

        assume

         A2: a in ( mi (( mi A) ^ B));

         A3:

        now

          let b be finite set;

          assume b in (A ^ B);

          then

          consider c be finite set such that

           A4: c c= b and

           A5: c in (( mi A) ^ B) by Lm2;

          assume

           A6: b c= a;

          then c c= a by A4;

          then c = a by A2, A5, Th6;

          hence b = a by A4, A6;

        end;

        a in (( mi A) ^ B) & a is finite by A2, Lm1, Th6;

        hence a in ( mi (A ^ B)) by A1, A3, Th7;

      end;

      hence ( mi (( mi A) ^ B)) c= ( mi (A ^ B));

      

       A7: ( mi (A ^ B)) c= (( mi A) ^ B) by Th17;

      now

        let a be set;

        assume

         A8: a in ( mi (A ^ B));

        then a is finite & for b be finite set st b in (( mi A) ^ B) holds b c= a implies b = a by A1, Lm1, Th6;

        hence a in ( mi (( mi A) ^ B)) by A7, A8, Th7;

      end;

      hence thesis;

    end;

    theorem :: SUBSTLAT:20

    

     Th20: ( mi (A ^ ( mi B))) = ( mi (A ^ B))

    proof

      (A ^ ( mi B)) = (( mi B) ^ A) & (A ^ B) = (B ^ A) by Th3;

      hence thesis by Th19;

    end;

    theorem :: SUBSTLAT:21

    

     Th21: for K,L,M be Element of ( Fin ( PFuncs (V,C))) holds (K ^ (L ^ M)) = ((K ^ L) ^ M)

    proof

      let K,L,M be Element of ( Fin ( PFuncs (V,C)));

      

       A1: (L ^ M) = (M ^ L) & (K ^ L) = (L ^ K) by Th3;

       A2:

      now

        let K,L,M be Element of ( Fin ( PFuncs (V,C)));

        

         A3: K c= ( PFuncs (V,C)) & L c= ( PFuncs (V,C)) by FINSUB_1:def 5;

        

         A4: M c= ( PFuncs (V,C)) by FINSUB_1:def 5;

        now

          let a be set;

          

           A5: (K ^ (L ^ M)) c= ( PFuncs (V,C)) by FINSUB_1:def 5;

          assume

           A6: a in (K ^ (L ^ M));

          then

          consider b,c be set such that

           A7: b in K and

           A8: c in (L ^ M) and

           A9: a = (b \/ c) by Th15;

          

           A10: c c= (b \/ c) by XBOOLE_1: 7;

          consider b1,c1 be set such that

           A11: b1 in L and

           A12: c1 in M and

           A13: c = (b1 \/ c1) by A8, Th15;

          reconsider b2 = b, b12 = b1 as PartFunc of V, C by A3, A7, A11, PARTFUN1: 46;

          reconsider b9 = b, b19 = b1, c19 = c1 as Element of ( PFuncs (V,C)) by A3, A4, A7, A11, A12;

          b1 c= c by A13, XBOOLE_1: 7;

          then

           A14: b c= (b \/ c) & b1 c= (b \/ c) by A10, XBOOLE_1: 7;

          then

           A15: b9 tolerates b19 by A6, A9, A5, PARTFUN1: 57;

          then (b9 \/ b19) = (b9 +* b19) by FUNCT_4: 30;

          then (b2 \/ b12) is PartFunc of V, C;

          then

          reconsider c2 = (b9 \/ b19) as Element of ( PFuncs (V,C)) by PARTFUN1: 45;

          

           A16: (b \/ (b1 \/ c1)) = ((b \/ b1) \/ c1) & c2 in (K ^ L) by A7, A11, A15, XBOOLE_1: 4;

          c1 c= c by A13, XBOOLE_1: 7;

          then

           A17: c1 c= (b \/ c) by A10;

          c2 c= (b \/ c) by A14, XBOOLE_1: 8;

          then c2 tolerates c19 by A6, A9, A5, A17, PARTFUN1: 57;

          hence a in ((K ^ L) ^ M) by A9, A12, A13, A16;

        end;

        hence (K ^ (L ^ M)) c= ((K ^ L) ^ M);

      end;

      then

       A18: (K ^ (L ^ M)) c= ((K ^ L) ^ M);

      ((K ^ L) ^ M) = (M ^ (K ^ L)) & (K ^ (L ^ M)) = ((L ^ M) ^ K) by Th3;

      then ((K ^ L) ^ M) c= (K ^ (L ^ M)) by A1, A2;

      hence thesis by A18;

    end;

    theorem :: SUBSTLAT:22

    

     Th22: for K,L,M be Element of ( Fin ( PFuncs (V,C))) holds (K ^ (L \/ M)) = ((K ^ L) \/ (K ^ M))

    proof

      let K,L,M be Element of ( Fin ( PFuncs (V,C)));

      now

        let a be set;

        assume

         A1: a in (K ^ (L \/ M));

        then

        consider b,c be set such that

         A2: b in K and

         A3: c in (L \/ M) and

         A4: a = (b \/ c) by Th15;

        (K ^ (L \/ M)) c= ( PFuncs (V,C)) by FINSUB_1:def 5;

        then

        reconsider a9 = a as Element of ( PFuncs (V,C)) by A1;

        K c= ( PFuncs (V,C)) & (L \/ M) c= ( PFuncs (V,C)) by FINSUB_1:def 5;

        then

        reconsider b9 = b, c9 = c as Element of ( PFuncs (V,C)) by A2, A3;

        b9 c= a9 & c9 c= a9 by A4, XBOOLE_1: 7;

        then

         A5: b9 tolerates c9 by PARTFUN1: 57;

        c9 in L or c9 in M by A3, XBOOLE_0:def 3;

        then a in (K ^ L) or a in (K ^ M) by A2, A4, A5;

        hence a in ((K ^ L) \/ (K ^ M)) by XBOOLE_0:def 3;

      end;

      hence (K ^ (L \/ M)) c= ((K ^ L) \/ (K ^ M));

      (K ^ L) c= (K ^ (L \/ M)) & (K ^ M) c= (K ^ (L \/ M)) by Th18, XBOOLE_1: 7;

      hence thesis by XBOOLE_1: 8;

    end;

    

     Lm3: for a be set holds a in (A ^ B) implies ex c be set st c in B & c c= a

    proof

      let a be set;

      assume a in (A ^ B);

      then

      consider b,c be set such that b in A and

       A1: c in B and

       A2: a = (b \/ c) by Th15;

      take c;

      thus c in B by A1;

      thus thesis by A2, XBOOLE_1: 7;

    end;

    

     Lm4: for K,L be Element of ( Fin ( PFuncs (V,C))) holds ( mi ((K ^ L) \/ L)) = ( mi L)

    proof

      let K,L be Element of ( Fin ( PFuncs (V,C)));

      now

        let a be set;

        assume

         A1: a in ( mi ((K ^ L) \/ L));

        then a in ((K ^ L) \/ L) by Th6;

        then

         A2: a in (K ^ L) or a in L by XBOOLE_0:def 3;

         A3:

        now

          let b be finite set;

          assume b in L;

          then b in ((K ^ L) \/ L) by XBOOLE_0:def 3;

          hence b c= a implies b = a by A1, Th6;

        end;

         A4:

        now

          assume a in (K ^ L);

          then

          consider b be set such that

           A5: b in L and

           A6: b c= a by Lm3;

          b in ((K ^ L) \/ L) by A5, XBOOLE_0:def 3;

          hence a in L by A1, A5, A6, Th6;

        end;

        a is finite by A1, Lm1;

        hence a in ( mi L) by A2, A4, A3, Th7;

      end;

      hence ( mi ((K ^ L) \/ L)) c= ( mi L);

      now

        let a be set;

        assume

         A7: a in ( mi L);

        then

         A8: a in L by Th6;

        then

         A9: a in ((K ^ L) \/ L) by XBOOLE_0:def 3;

         A10:

        now

          let b be finite set;

          assume b in ((K ^ L) \/ L);

          then

           A11: b in (K ^ L) or b in L by XBOOLE_0:def 3;

          assume

           A12: b c= a;

          now

            assume b in (K ^ L);

            then

            consider c be set such that

             A13: c in L and

             A14: c c= b by Lm3;

            c c= a by A12, A14;

            then c = a by A7, A13, Th6;

            hence b in L by A8, A12, A14, XBOOLE_0:def 10;

          end;

          hence b = a by A7, A11, A12, Th6;

        end;

        a is finite by A7, Lm1;

        hence a in ( mi ((K ^ L) \/ L)) by A9, A10, Th7;

      end;

      hence thesis;

    end;

    theorem :: SUBSTLAT:23

    

     Th23: B c= (B ^ B)

    proof

      now

        let a be set;

        assume

         A1: a in B;

        B c= ( PFuncs (V,C)) by FINSUB_1:def 5;

        then

        reconsider a9 = a as Element of ( PFuncs (V,C)) by A1;

        a = (a \/ a) & a9 tolerates a9;

        hence a in (B ^ B) by A1;

      end;

      hence thesis;

    end;

    theorem :: SUBSTLAT:24

    

     Th24: ( mi (A ^ A)) = ( mi A)

    proof

      

      thus ( mi (A ^ A)) = ( mi ((A ^ A) \/ A)) by Th23, XBOOLE_1: 12

      .= ( mi A) by Lm4;

    end;

    theorem :: SUBSTLAT:25

    for K be Element of ( SubstitutionSet (V,C)) holds ( mi (K ^ K)) = K

    proof

      let K be Element of ( SubstitutionSet (V,C));

      

      thus ( mi (K ^ K)) = ( mi K) by Th24

      .= K by Th11;

    end;

    begin

    definition

      let V, C;

      :: SUBSTLAT:def4

      func SubstLatt (V,C) -> strict LattStr means

      : Def4: the carrier of it = ( SubstitutionSet (V,C)) & for A,B be Element of ( SubstitutionSet (V,C)) holds (the L_join of it . (A,B)) = ( mi (A \/ B)) & (the L_meet of it . (A,B)) = ( mi (A ^ B));

      existence

      proof

        deffunc U( Element of ( SubstitutionSet (V,C)), Element of ( SubstitutionSet (V,C))) = ( mi ($1 \/ $2));

        consider j be BinOp of ( SubstitutionSet (V,C)) such that

         A1: for x,y be Element of ( SubstitutionSet (V,C)) holds (j . (x,y)) = U(x,y) from BINOP_1:sch 4;

        deffunc U( Element of ( SubstitutionSet (V,C)), Element of ( SubstitutionSet (V,C))) = ( mi ($1 ^ $2));

        consider m be BinOp of ( SubstitutionSet (V,C)) such that

         A2: for x,y be Element of ( SubstitutionSet (V,C)) holds (m . (x,y)) = U(x,y) from BINOP_1:sch 4;

        take LattStr (# ( SubstitutionSet (V,C)), j, m #);

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let A1,A2 be strict LattStr such that

         A3: the carrier of A1 = ( SubstitutionSet (V,C)) and

         A4: for A,B be Element of ( SubstitutionSet (V,C)) holds (the L_join of A1 . (A,B)) = ( mi (A \/ B)) & (the L_meet of A1 . (A,B)) = ( mi (A ^ B)) and

         A5: the carrier of A2 = ( SubstitutionSet (V,C)) and

         A6: for A,B be Element of ( SubstitutionSet (V,C)) holds (the L_join of A2 . (A,B)) = ( mi (A \/ B)) & (the L_meet of A2 . (A,B)) = ( mi (A ^ B));

        reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of ( SubstitutionSet (V,C)) by A3, A5;

        now

          let x,y be Element of ( SubstitutionSet (V,C));

          

          thus (a1 . (x,y)) = ( mi (x \/ y)) by A4

          .= (a2 . (x,y)) by A6;

        end;

        then

         A7: a1 = a2 by BINOP_1: 2;

        now

          let x,y be Element of ( SubstitutionSet (V,C));

          

          thus (a3 . (x,y)) = ( mi (x ^ y)) by A4

          .= (a4 . (x,y)) by A6;

        end;

        hence thesis by A3, A5, A7, BINOP_1: 2;

      end;

    end

    registration

      let V, C;

      cluster ( SubstLatt (V,C)) -> non empty;

      coherence

      proof

        the carrier of ( SubstLatt (V,C)) = ( SubstitutionSet (V,C)) by Def4;

        hence thesis;

      end;

    end

    

     Lm5: for a,b be Element of ( SubstLatt (V,C)) holds (a "\/" b) = (b "\/" a)

    proof

      set G = ( SubstLatt (V,C));

      let a,b be Element of G;

      reconsider a9 = a, b9 = b as Element of ( SubstitutionSet (V,C)) by Def4;

      (a "\/" b) = ( mi (b9 \/ a9)) by Def4

      .= (b "\/" a) by Def4;

      hence thesis;

    end;

    

     Lm6: for a,b,c be Element of ( SubstLatt (V,C)) holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c)

    proof

      let a,b,c be Element of ( SubstLatt (V,C));

      reconsider a9 = a, b9 = b, c9 = c as Element of ( SubstitutionSet (V,C)) by Def4;

      set G = ( SubstLatt (V,C));

      (a "\/" (b "\/" c)) = (the L_join of G . (a,( mi (b9 \/ c9)))) by Def4

      .= ( mi (( mi (b9 \/ c9)) \/ a9)) by Def4

      .= ( mi (a9 \/ (b9 \/ c9))) by Th13

      .= ( mi ((a9 \/ b9) \/ c9)) by XBOOLE_1: 4

      .= ( mi (( mi (a9 \/ b9)) \/ c9)) by Th13

      .= (the L_join of G . (( mi (a9 \/ b9)),c9)) by Def4

      .= ((a "\/" b) "\/" c) by Def4;

      hence thesis;

    end;

    reserve K,L,M for Element of ( SubstitutionSet (V,C));

    

     Lm7: (the L_join of ( SubstLatt (V,C)) . ((the L_meet of ( SubstLatt (V,C)) . (K,L)),L)) = L

    proof

      

      thus (the L_join of ( SubstLatt (V,C)) . ((the L_meet of ( SubstLatt (V,C)) . (K,L)),L)) = (the L_join of ( SubstLatt (V,C)) . (( mi (K ^ L)),L)) by Def4

      .= ( mi (( mi (K ^ L)) \/ L)) by Def4

      .= ( mi ((K ^ L) \/ L)) by Th13

      .= ( mi L) by Lm4

      .= L by Th11;

    end;

    

     Lm8: for a,b be Element of ( SubstLatt (V,C)) holds ((a "/\" b) "\/" b) = b

    proof

      let a,b be Element of ( SubstLatt (V,C));

      reconsider a9 = a, b9 = b as Element of ( SubstitutionSet (V,C)) by Def4;

      set G = ( SubstLatt (V,C));

      

      thus ((a "/\" b) "\/" b) = (the L_join of G . ((the L_meet of G . (a9,b9)),b9))

      .= b by Lm7;

    end;

    

     Lm9: for a,b be Element of ( SubstLatt (V,C)) holds (a "/\" b) = (b "/\" a)

    proof

      let a,b be Element of ( SubstLatt (V,C));

      reconsider a9 = a, b9 = b as Element of ( SubstitutionSet (V,C)) by Def4;

      (a "/\" b) = ( mi (a9 ^ b9)) by Def4

      .= ( mi (b9 ^ a9)) by Th3

      .= (b "/\" a) by Def4;

      hence thesis;

    end;

    

     Lm10: for a,b,c be Element of ( SubstLatt (V,C)) holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)

    proof

      let a,b,c be Element of ( SubstLatt (V,C));

      reconsider a9 = a, b9 = b, c9 = c as Element of ( SubstitutionSet (V,C)) by Def4;

      set G = ( SubstLatt (V,C));

      (a "/\" (b "/\" c)) = (the L_meet of G . (a,( mi (b9 ^ c9)))) by Def4

      .= ( mi (a9 ^ ( mi (b9 ^ c9)))) by Def4

      .= ( mi (a9 ^ (b9 ^ c9))) by Th20

      .= ( mi ((a9 ^ b9) ^ c9)) by Th21

      .= ( mi (( mi (a9 ^ b9)) ^ c9)) by Th19

      .= (the L_meet of G . (( mi (a9 ^ b9)),c9)) by Def4

      .= ((a "/\" b) "/\" c) by Def4;

      hence thesis;

    end;

    

     Lm11: (the L_meet of ( SubstLatt (V,C)) . (K,(the L_join of ( SubstLatt (V,C)) . (L,M)))) = (the L_join of ( SubstLatt (V,C)) . ((the L_meet of ( SubstLatt (V,C)) . (K,L)),(the L_meet of ( SubstLatt (V,C)) . (K,M))))

    proof

      

       A1: (the L_meet of ( SubstLatt (V,C)) . (K,M)) = ( mi (K ^ M)) by Def4;

      (the L_join of ( SubstLatt (V,C)) . (L,M)) = ( mi (L \/ M)) & (the L_meet of ( SubstLatt (V,C)) . (K,L)) = ( mi (K ^ L)) by Def4;

      then

      reconsider La = (the L_join of ( SubstLatt (V,C)) . (L,M)), Lb = (the L_meet of ( SubstLatt (V,C)) . (K,L)), Lc = (the L_meet of ( SubstLatt (V,C)) . (K,M)) as Element of ( SubstitutionSet (V,C)) by A1;

      (the L_meet of ( SubstLatt (V,C)) . (K,(the L_join of ( SubstLatt (V,C)) . (L,M)))) = ( mi (K ^ La)) by Def4

      .= ( mi (K ^ ( mi (L \/ M)))) by Def4

      .= ( mi (K ^ (L \/ M))) by Th20

      .= ( mi ((K ^ L) \/ (K ^ M))) by Th22

      .= ( mi (( mi (K ^ L)) \/ (K ^ M))) by Th13

      .= ( mi (( mi (K ^ L)) \/ ( mi (K ^ M)))) by Th13

      .= ( mi (Lb \/ ( mi (K ^ M)))) by Def4

      .= ( mi (Lb \/ Lc)) by Def4;

      hence thesis by Def4;

    end;

    

     Lm12: for a,b be Element of ( SubstLatt (V,C)) holds (a "/\" (a "\/" b)) = a

    proof

      let a,b be Element of ( SubstLatt (V,C));

      reconsider a9 = a, b9 = b as Element of ( SubstitutionSet (V,C)) by Def4;

      

      thus (a "/\" (a "\/" b)) = (the L_join of ( SubstLatt (V,C)) . ((the L_meet of ( SubstLatt (V,C)) . (a9,a9)),(the L_meet of ( SubstLatt (V,C)) . (a9,b9)))) by Lm11

      .= (the L_join of ( SubstLatt (V,C)) . (( mi (a9 ^ a9)),(the L_meet of ( SubstLatt (V,C)) . (a9,b9)))) by Def4

      .= (the L_join of ( SubstLatt (V,C)) . (( mi a9),(the L_meet of ( SubstLatt (V,C)) . (a9,b9)))) by Th24

      .= (a "\/" (a "/\" b)) by Th11

      .= ((a "/\" b) "\/" a) by Lm5

      .= ((b "/\" a) "\/" a) by Lm9

      .= a by Lm8;

    end;

    registration

      let V, C;

      cluster ( SubstLatt (V,C)) -> Lattice-like;

      coherence

      proof

        set G = ( SubstLatt (V,C));

        thus for u,v be Element of G holds (u "\/" v) = (v "\/" u) by Lm5;

        thus for u,v,w be Element of G holds (u "\/" (v "\/" w)) = ((u "\/" v) "\/" w) by Lm6;

        thus for u,v be Element of G holds ((u "/\" v) "\/" v) = v by Lm8;

        thus for u,v be Element of G holds (u "/\" v) = (v "/\" u) by Lm9;

        thus for u,v,w be Element of G holds (u "/\" (v "/\" w)) = ((u "/\" v) "/\" w) by Lm10;

        let u,v be Element of G;

        thus thesis by Lm12;

      end;

    end

    registration

      let V, C;

      cluster ( SubstLatt (V,C)) -> distributive bounded;

      coherence

      proof

        thus ( SubstLatt (V,C)) is distributive

        proof

          let u,v,w be Element of ( SubstLatt (V,C));

          reconsider K = u, L = v, M = w as Element of ( SubstitutionSet (V,C)) by Def4;

          

          thus (u "/\" (v "\/" w)) = (the L_meet of ( SubstLatt (V,C)) . (K,(the L_join of ( SubstLatt (V,C)) . (L,M))))

          .= ((u "/\" v) "\/" (u "/\" w)) by Lm11;

        end;

        

         A1: ( SubstLatt (V,C)) is lower-bounded

        proof

          reconsider E = {} as Element of ( SubstitutionSet (V,C)) by Th1;

          set L = ( SubstLatt (V,C));

          reconsider e = E as Element of L by Def4;

          take e;

          let u be Element of L;

          reconsider K = u as Element of ( SubstitutionSet (V,C)) by Def4;

          

           A2: (e "\/" u) = ( mi (E \/ K)) by Def4

          .= u by Th11;

          then (u "/\" e) = e by LATTICES:def 9;

          hence thesis by A2, LATTICES:def 9;

        end;

        ( SubstLatt (V,C)) is upper-bounded

        proof

          reconsider E = { {} } as Element of ( SubstitutionSet (V,C)) by Th2;

          set L = ( SubstLatt (V,C));

          reconsider e = E as Element of L by Def4;

          take e;

          let u be Element of L;

          reconsider K = u as Element of ( SubstitutionSet (V,C)) by Def4;

          

           A3: (e "/\" u) = ( mi (E ^ K)) by Def4

          .= ( mi (K ^ E)) by Th3

          .= ( mi K) by Th4

          .= u by Th11;

          then (e "\/" u) = e by LATTICES:def 8;

          hence thesis by A3, LATTICES:def 8;

        end;

        hence ( SubstLatt (V,C)) is bounded by A1;

      end;

    end

    theorem :: SUBSTLAT:26

    ( Bottom ( SubstLatt (V,C))) = {}

    proof

       {} in ( SubstitutionSet (V,C)) by Th1;

      then

      reconsider Z = {} as Element of ( SubstLatt (V,C)) by Def4;

      now

        let u be Element of ( SubstLatt (V,C));

        reconsider z = Z, u9 = u as Element of ( SubstitutionSet (V,C)) by Def4;

        

        thus (Z "\/" u) = ( mi (z \/ u9)) by Def4

        .= u by Th11;

      end;

      hence thesis by LATTICE2: 14;

    end;

    theorem :: SUBSTLAT:27

    ( Top ( SubstLatt (V,C))) = { {} }

    proof

       { {} } in ( SubstitutionSet (V,C)) by Th2;

      then

      reconsider Z = { {} } as Element of ( SubstLatt (V,C)) by Def4;

      now

        let u be Element of ( SubstLatt (V,C));

        reconsider z = Z, u9 = u as Element of ( SubstitutionSet (V,C)) by Def4;

        

        thus (Z "/\" u) = ( mi (z ^ u9)) by Def4

        .= ( mi (u9 ^ z)) by Th3

        .= ( mi u9) by Th4

        .= u by Th11;

      end;

      hence thesis by LATTICE2: 16;

    end;