heyting2.miz



    begin

    reserve V,C,x,a,b for set;

    reserve A,B for Element of ( SubstitutionSet (V,C));

    theorem :: HEYTING2:1

    

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

    proof

      let a,b be set;

      assume that

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

       A2: a in b;

      b in { A where A be Element of ( Fin ( PFuncs (V,C))) : (for u be set st u in A holds u is finite) & for s1,t be Element of ( PFuncs (V,C)) holds (s1 in A & t in A & s1 c= t implies s1 = t) } by A1, SUBSTLAT:def 1;

      then 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);

      hence thesis by A1, A2;

    end;

    

     Lm1: for A,B,C be set st A = (B \/ C) & A c= B holds A = B by XBOOLE_1: 7;

    begin

    theorem :: HEYTING2:2

    

     Th2: for a be finite Element of ( PFuncs (V,C)) holds {a} in ( SubstitutionSet (V,C))

    proof

      let a be finite Element of ( PFuncs (V,C));

      

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

      proof

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

        assume that

         A2: s in {a} and

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

        s = a by A2, TARSKI:def 1;

        hence thesis by A3, TARSKI:def 1;

      end;

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

      then {.a.} in { 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) } by A1;

      hence thesis by SUBSTLAT:def 1;

    end;

    theorem :: HEYTING2:3

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

    proof

      assume

       A1: (A ^ B) = A;

      let a be set;

      assume a in A;

      then

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

       A2: c in B and

       A3: a = (b \/ c) by A1, SUBSTLAT: 15;

      take c;

      thus thesis by A2, A3, XBOOLE_1: 7;

    end;

    theorem :: HEYTING2:4

    

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

    proof

      assume

       A1: ( mi (A ^ B)) = A;

      let a be set;

      

       A2: ( mi (A ^ B)) c= (A ^ B) by SUBSTLAT: 8;

      assume a in A;

      then

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

       A3: c in B and

       A4: a = (b \/ c) by A1, A2, SUBSTLAT: 15;

      take c;

      thus thesis by A3, A4, XBOOLE_1: 7;

    end;

    theorem :: HEYTING2:5

    

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

    proof

      assume

       A1: for a be set st a in A holds ex b be set st b in B & b c= a;

      

       A2: ( mi (A ^ B)) c= (A ^ B) by SUBSTLAT: 8;

      thus ( mi (A ^ B)) c= A

      proof

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        

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

        assume

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

        then

        consider b,c be set such that

         A5: b in A and c in B and

         A6: a = (b \/ c) by A2, SUBSTLAT: 15;

        

         A7: b c= aa by A6, XBOOLE_1: 7;

        consider b1 be set such that

         A8: b1 in B and

         A9: b1 c= b by A1, A5;

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

        then

        reconsider b9 = b, b19 = b1 as Element of ( PFuncs (V,C)) by A5, A8, A3;

        

         A10: b = (b1 \/ b) by A9, XBOOLE_1: 12;

        b19 tolerates b9 by A9, PARTFUN1: 54;

        then b in (A ^ B) by A5, A8, A10, SUBSTLAT: 16;

        hence thesis by A4, A5, A7, SUBSTLAT: 6;

      end;

      thus A c= ( mi (A ^ B))

      proof

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        

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

        assume

         A12: a in A;

        then

        consider b be set such that

         A13: b in B and

         A14: b c= aa by A1;

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

        then

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

        

         A15: a9 tolerates b9 by A14, PARTFUN1: 54;

        

         A16: a in ( mi A) by A12, SUBSTLAT: 11;

        

         A17: for b be finite set st b in (A ^ B) & b c= aa holds b = a

        proof

          let b be finite set;

          assume that

           A18: b in (A ^ B) and

           A19: b c= aa;

          consider c,d be set such that

           A20: c in A and d in B and

           A21: b = (c \/ d) by A18, SUBSTLAT: 15;

          c c= b by A21, XBOOLE_1: 7;

          then c c= aa by A19;

          then c = a by A16, A20, SUBSTLAT: 6;

          hence thesis by A19, A21, Lm1;

        end;

        a9 = (a9 \/ b9) by A14, XBOOLE_1: 12;

        then

         A22: a9 in (A ^ B) by A12, A13, A15, SUBSTLAT: 16;

        aa is finite by A12, Th1;

        hence thesis by A22, A17, SUBSTLAT: 7;

      end;

    end;

    definition

      let V be set, C be finite set;

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

      :: HEYTING2:def1

      func Involved A -> set means

      : Def1: for x be object holds x in it iff ex f be finite Function st f in A & x in ( dom f);

      existence

      proof

        defpred P[ object] means ex f be finite Function st f in A & $1 in ( dom f);

        consider X be set such that

         A1: for x be object holds x in X iff x in V & P[x] from XBOOLE_0:sch 1;

        take X;

        let x be object;

        thus x in X implies ex f be finite Function st f in A & x in ( dom f) by A1;

        given f be finite Function such that

         A2: f in A and

         A3: x in ( dom f);

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

        then ex f1 be Function st f = f1 & ( dom f1) c= V & ( rng f1) c= C by A2, PARTFUN1:def 3;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        defpred P[ object] means ex f be finite Function st f in A & $1 in ( dom f);

        let r,s be set such that

         A4: for x be object holds x in r iff ex f be finite Function st f in A & x in ( dom f) and

         A5: for x be object holds x in s iff ex f be finite Function st f in A & x in ( dom f);

        for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

        hence thesis by A4, A5;

      end;

    end

    reserve C for finite set;

    reserve A,B for Element of ( SubstitutionSet (V,C));

    theorem :: HEYTING2:6

    

     Th6: for V be set, C be finite set, A be Element of ( Fin ( PFuncs (V,C))) holds ( Involved A) c= V

    proof

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

      let a be object;

      assume a in ( Involved A);

      then

      consider f be finite Function such that

       A1: f in A and

       A2: a in ( dom f) by Def1;

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

      then ex f1 be Function st f = f1 & ( dom f1) c= V & ( rng f1) c= C by A1, PARTFUN1:def 3;

      hence thesis by A2;

    end;

    

     Lm2: for V be set, C be finite set, A be non empty Element of ( Fin ( PFuncs (V,C))) holds ( Involved A) is finite

    proof

      deffunc F( Function) = ( dom $1);

      let V be set, C be finite set, A be non empty Element of ( Fin ( PFuncs (V,C)));

      defpred P[ set] means $1 in A & $1 is finite;

      defpred Q[ set] means $1 in A;

      set X = { F(f) where f be Element of ( PFuncs (V,C)) : P[f] };

      

       A1: for x be set st x in X holds x is finite

      proof

        let x be set;

        assume x in X;

        then ex f1 be Element of ( PFuncs (V,C)) st x = ( dom f1) & f1 in A & f1 is finite;

        hence thesis;

      end;

      

       A2: A is finite;

      

       A3: { F(f) where f be Element of ( PFuncs (V,C)) : f in A } is finite from FRAENKEL:sch 21( A2);

      for x be object holds x in ( Involved A) iff ex Y be set st x in Y & Y in X

      proof

        let x be object;

        hereby

          assume x in ( Involved A);

          then

          consider f be finite Function such that

           A4: f in A and

           A5: x in ( dom f) by Def1;

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

          then ( dom f) in X by A4;

          hence ex Y be set st x in Y & Y in X by A5;

        end;

        given Y be set such that

         A6: x in Y and

         A7: Y in X;

        ex f1 be Element of ( PFuncs (V,C)) st Y = ( dom f1) & f1 in A & f1 is finite by A7;

        hence thesis by A6, Def1;

      end;

      then

       A8: ( Involved A) = ( union X) by TARSKI:def 4;

      

       A9: for g be Element of ( PFuncs (V,C)) holds P[g] implies Q[g];

      X c= { F(f) where f be Element of ( PFuncs (V,C)) : Q[f] } from FRAENKEL:sch 1( A9);

      hence thesis by A3, A8, A1, FINSET_1: 7;

    end;

    theorem :: HEYTING2:7

    

     Th7: for V be set, C be finite set, A be Element of ( Fin ( PFuncs (V,C))) st A = {} holds ( Involved A) = {}

    proof

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

      assume

       A1: A = {} ;

      assume ( Involved A) <> {} ;

      then

      consider x be object such that

       A2: x in ( Involved A) by XBOOLE_0:def 1;

      ex f be finite Function st f in A & x in ( dom f) by A2, Def1;

      hence thesis by A1;

    end;

    registration

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

      cluster ( Involved A) -> finite;

      coherence

      proof

        per cases ;

          suppose A is non empty;

          hence thesis by Lm2;

        end;

          suppose A is empty;

          hence thesis by Th7;

        end;

      end;

    end

    theorem :: HEYTING2:8

    for C be finite set, A be Element of ( Fin ( PFuncs ( {} ,C))) holds ( Involved A) = {} by Th6, XBOOLE_1: 3;

    definition

      let V be set, C be finite set;

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

      :: HEYTING2:def2

      func - A -> Element of ( Fin ( PFuncs (V,C))) equals { f where f be Element of ( PFuncs (( Involved A),C)) : for g be Element of ( PFuncs (V,C)) st g in A holds not f tolerates g };

      coherence

      proof

        deffunc F( set) = $1;

        defpred Q[ set] means not contradiction;

        defpred P[ Element of ( PFuncs (( Involved A),C))] means for h be Element of ( PFuncs (V,C)) st h in A holds not $1 tolerates h;

        set M = { f where f be Element of ( PFuncs (( Involved A),C)) : for g be Element of ( PFuncs (V,C)) st g in A holds not f tolerates g };

        

         A1: the set of all f where f be Element of ( PFuncs (( Involved A),C)) c= ( PFuncs (( Involved A),C))

        proof

          let a be object;

          assume a in the set of all f where f be Element of ( PFuncs (( Involved A),C));

          then ex f1 be Element of ( PFuncs (( Involved A),C)) st f1 = a & not contradiction;

          hence thesis;

        end;

        

         A2: for v be Element of ( PFuncs (( Involved A),C)) holds P[v] implies Q[v];

        

         A3: { F(f) where f be Element of ( PFuncs (( Involved A),C)) : P[f] } c= { F(f) where f be Element of ( PFuncs (( Involved A),C)) : Q[f] } from FRAENKEL:sch 1( A2);

        

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

        proof

          let a be object;

          assume a in M;

          then ex f1 be Element of ( PFuncs (( Involved A),C)) st f1 = a & for g be Element of ( PFuncs (V,C)) st g in A holds not f1 tolerates g;

          then

           A5: a in ( PFuncs (( Involved A),C));

          ( Involved A) c= V by Th6;

          then ( PFuncs (( Involved A),C)) c= ( PFuncs (V,C)) by PARTFUN1: 50;

          hence thesis by A5;

        end;

        ( PFuncs (( Involved A),C)) is finite by PRE_POLY: 17;

        hence thesis by A3, A1, A4, FINSUB_1:def 5;

      end;

    end

    theorem :: HEYTING2:9

    

     Th9: (A ^ ( - A)) = {}

    proof

      assume (A ^ ( - A)) <> {} ;

      then

      consider x be object such that

       A1: x in (A ^ ( - A)) by XBOOLE_0:def 1;

      x in { (s \/ t) where s,t be Element of ( PFuncs (V,C)) : s in A & t in ( - A) & s tolerates t } by A1, SUBSTLAT:def 3;

      then

      consider s1,t1 be Element of ( PFuncs (V,C)) such that x = (s1 \/ t1) and

       A2: s1 in A and

       A3: t1 in ( - A) and

       A4: s1 tolerates t1;

      ex f1 be Element of ( PFuncs (( Involved A),C)) st f1 = t1 & for g be Element of ( PFuncs (V,C)) st g in A holds not f1 tolerates g by A3;

      hence thesis by A2, A4;

    end;

    theorem :: HEYTING2:10

    

     Th10: A = {} implies ( - A) = { {} }

    proof

      defpred P[ Element of ( PFuncs (( Involved A),C))] means for g be Element of ( PFuncs (V,C)) st g in A holds not $1 tolerates g;

      assume

       A1: A = {} ;

      then

       A2: for g be Element of ( PFuncs (V,C)) st g in A holds not {} tolerates g;

      { xx where xx be Element of ( PFuncs (( Involved A),C)) : P[xx] } c= ( PFuncs (( Involved A),C)) from FRAENKEL:sch 10;

      then ( - A) c= ( PFuncs ( {} ,C)) by A1, Th7;

      then

       A3: ( - A) c= { {} } by PARTFUN1: 48;

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

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

      then {} in ( PFuncs (( Involved A),C)) by A1, Th7;

      then {} in ( - A) by A2;

      then { {} } c= ( - A) by ZFMISC_1: 31;

      hence thesis by A3;

    end;

    theorem :: HEYTING2:11

    A = { {} } implies ( - A) = {}

    proof

      assume

       A1: A = { {} };

      assume ( - A) <> {} ;

      then

      consider x1 be object such that

       A2: x1 in ( - A) by XBOOLE_0:def 1;

      consider f1 be Element of ( PFuncs (( Involved A),C)) such that x1 = f1 and

       A3: for g be Element of ( PFuncs (V,C)) st g in { {} } holds not f1 tolerates g by A1, A2;

      

       A4: {} in { {} } by TARSKI:def 1;

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

      then

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

      f1 tolerates {} by PARTFUN1: 59;

      hence thesis by A3, A5, A4;

    end;

    theorem :: HEYTING2:12

    

     Th12: for V be set, C be finite set holds for A be Element of ( SubstitutionSet (V,C)) holds ( mi (A ^ ( - A))) = ( Bottom ( SubstLatt (V,C)))

    proof

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

      ( mi (A ^ ( - A))) = {} by Th9, SUBSTLAT: 9

      .= ( Bottom ( SubstLatt (V,C))) by SUBSTLAT: 26;

      hence thesis;

    end;

    theorem :: HEYTING2:13

    for V be non empty set, C be finite non empty set holds for A be Element of ( SubstitutionSet (V,C)) st A = {} holds ( mi ( - A)) = ( Top ( SubstLatt (V,C)))

    proof

      let V be non empty set, C be finite non empty set, A be Element of ( SubstitutionSet (V,C));

      assume A = {} ;

      then

       A1: ( - A) = { {} } by Th10;

      then ( - A) in ( SubstitutionSet (V,C)) by SUBSTLAT: 2;

      then ( mi ( - A)) = { {} } by A1, SUBSTLAT: 11;

      hence thesis by SUBSTLAT: 27;

    end;

    theorem :: HEYTING2:14

    

     Th14: for V be set, C be finite set holds for A be Element of ( SubstitutionSet (V,C)), a be Element of ( PFuncs (V,C)), B be Element of ( SubstitutionSet (V,C)) st B = {a} holds (A ^ B) = {} implies ex b be finite set st b in ( - A) & b c= a

    proof

      let V, C;

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

      let a be Element of ( PFuncs (V,C));

      let B be Element of ( SubstitutionSet (V,C)) such that

       A1: B = {a};

      assume

       A2: (A ^ B) = {} ;

      per cases ;

        suppose

         A3: A is non empty;

        then

        reconsider AA = A as finite non empty set;

        defpred P[ Element of ( PFuncs (V,C)), set] means $2 in (( dom $1) /\ ( dom a)) & ($1 . $2) <> (a . $2);

        defpred P[ set] means not contradiction;

        

         A4: ex kk be Function st kk = a & ( dom kk) c= V & ( rng kk) c= C by PARTFUN1:def 3;

         A5:

        now

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

           A6: s in A;

           not s tolerates a

          proof

            assume

             A7: s tolerates a;

            a in B by A1, TARSKI:def 1;

            then (s \/ a) in { (s1 \/ t1) where s1,t1 be Element of ( PFuncs (V,C)) : s1 in A & t1 in B & s1 tolerates t1 } by A6, A7;

            hence thesis by A2, SUBSTLAT:def 3;

          end;

          then

          consider x be object such that

           A8: x in (( dom s) /\ ( dom a)) and

           A9: (s . x) <> (a . x) by PARTFUN1:def 4;

          consider a9 be Function such that

           A10: a9 = a and

           A11: ( dom a9) c= V and ( rng a9) c= C by PARTFUN1:def 3;

          (( dom s) /\ ( dom a)) c= ( dom a9) by A10, XBOOLE_1: 17;

          then (( dom s) /\ ( dom a)) c= V by A11;

          then

          reconsider x as Element of [V] by A8, HEYTING1:def 2;

          take x;

          thus P[s, x] by A8, A9;

        end;

        consider g be Element of ( Funcs (( PFuncs (V,C)), [V])) such that

         A12: for s be Element of ( PFuncs (V,C)) st s in A holds P[s, (g . s)] from FRAENKEL:sch 27( A5);

        deffunc G( set) = (g . $1);

        

         A13: A = [A] by A3, HEYTING1:def 2;

        { G(b) where b be Element of AA : P[b] } is finite from PRE_CIRC:sch 1;

        then

        reconsider UKA = the set of all (g . b) where b be Element of [A] as finite set by A13;

        set f = (a | UKA);

        

         A14: ( dom f) c= ( Involved A)

        proof

          let x be object;

          assume x in ( dom f);

          then x in UKA by RELAT_1: 57;

          then

          consider b be Element of [A] such that

           A15: x = (g . b);

          reconsider b as finite Function by A13, Th1;

          reconsider b9 = b as Element of ( PFuncs (V,C)) by A13, SETWISEO: 9;

          (g . b9) in (( dom b9) /\ ( dom a)) by A13, A12;

          then x in ( dom b) by A15, XBOOLE_0:def 4;

          hence thesis by A13, Def1;

        end;

        ( rng f) c= ( rng a) by RELAT_1: 70;

        then ( rng f) c= C by A4;

        then

        reconsider f9 = f as Element of ( PFuncs (( Involved A),C)) by A14, PARTFUN1:def 3;

        for g be Element of ( PFuncs (V,C)) st g in A holds not f tolerates g

        proof

          let g1 be Element of ( PFuncs (V,C));

          reconsider g9 = g1 as Function;

          assume

           A16: g1 in A;

          ex z be set st z in (( dom g1) /\ ( dom f)) & (g9 . z) <> (f . z)

          proof

            set z = (g . g1);

            take z;

            

             A17: z in (( dom g1) /\ ( dom a)) by A12, A16;

            then

             A18: z in ( dom a) by XBOOLE_0:def 4;

            z in the set of all (g . b1) where b1 be Element of [A] by A13, A16;

            then z in (( dom a) /\ UKA) by A18, XBOOLE_0:def 4;

            then

             A19: z in ( dom f) by RELAT_1: 61;

            z in ( dom g1) by A17, XBOOLE_0:def 4;

            hence z in (( dom g1) /\ ( dom f)) by A19, XBOOLE_0:def 4;

            (g1 . z) <> (a . z) by A12, A16;

            hence thesis by A19, FUNCT_1: 47;

          end;

          hence thesis by PARTFUN1:def 4;

        end;

        then f9 in { f1 where f1 be Element of ( PFuncs (( Involved A),C)) : for g be Element of ( PFuncs (V,C)) st g in A holds not f1 tolerates g };

        hence thesis by RELAT_1: 59;

      end;

        suppose

         A20: A is empty;

        reconsider K = {} as finite set;

        take K;

        ( - A) = { {} } by A20, Th10;

        hence thesis by TARSKI:def 1;

      end;

    end;

    definition

      let V be set, C be finite set;

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

      :: HEYTING2:def3

      func A =>> B -> Element of ( Fin ( PFuncs (V,C))) equals (( PFuncs (V,C)) /\ { ( union { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A }) where f be Element of ( PFuncs (A,B)) : ( dom f) = A });

      coherence

      proof

        reconsider PF = ( PFuncs (A,B)) as functional finite non empty set by PRE_POLY: 17;

        set Z = { ( union { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A }) where f be Element of ( PFuncs (A,B)) : ( dom f) = A };

        set K = (( PFuncs (V,C)) /\ Z);

        

         A1: Z c= { ( union { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A }) where f be Element of ( PFuncs (A,B)) : f in ( PFuncs (A,B)) & ( dom f) = A }

        proof

          let z be object;

          assume z in Z;

          then ex f1 be Element of ( PFuncs (A,B)) st z = ( union { ((f1 . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A }) & ( dom f1) = A;

          hence thesis;

        end;

        defpred P[ Element of PF] means $1 in ( PFuncs (A,B)) & ( dom $1) = A;

        deffunc F( Element of PF) = ( union { (($1 . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A });

        

         A2: { F(f) where f be Element of PF : P[f] } is finite from PRE_CIRC:sch 1;

        K c= ( PFuncs (V,C)) by XBOOLE_1: 17;

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

      end;

    end

    theorem :: HEYTING2:15

    

     Th15: for A,B be Element of ( Fin ( PFuncs (V,C))), s be set st s in (A =>> B) holds ex f be PartFunc of A, B st s = ( union { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A }) & ( dom f) = A

    proof

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

      assume s in (A =>> B);

      then s in { ( union { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A }) where f be Element of ( PFuncs (A,B)) : ( dom f) = A } by XBOOLE_0:def 4;

      then

      consider f be Element of ( PFuncs (A,B)) such that

       A1: s = ( union { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A }) and

       A2: ( dom f) = A;

      f is PartFunc of A, B by PARTFUN1: 47;

      hence thesis by A1, A2;

    end;

    

     Lm3: for V be set, C be finite set, A be Element of ( Fin ( PFuncs (V,C))), K be Element of ( SubstitutionSet (V,C)) holds a in (A ^ (A =>> K)) implies ex b st b in K & b c= a

    proof

      let V be set, C be finite set, A be Element of ( Fin ( PFuncs (V,C))), K be Element of ( SubstitutionSet (V,C));

      

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

      assume a in (A ^ (A =>> K));

      then

      consider b,c be set such that

       A2: b in A and

       A3: c in (A =>> K) and

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

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

      then

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

      consider f be PartFunc of A, K such that

       A5: c = ( union { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A }) and

       A6: ( dom f) = A by A3, Th15;

      (f . b) in K by A2, A6, PARTFUN1: 4;

      then

      reconsider d = (f . b) as Element of ( PFuncs (V,C)) by A1;

      take d;

      thus d in K by A2, A6, PARTFUN1: 4;

      (d \ b9) in { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A } by A2;

      hence thesis by A4, A5, XBOOLE_1: 44, ZFMISC_1: 74;

    end;

    theorem :: HEYTING2:16

    for V be set, C be finite set, A be Element of ( Fin ( PFuncs (V,C))) st A = {} holds (A =>> A) = { {} }

    proof

      deffunc G( set) = {} ;

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

      defpred P[ Function] means ( dom $1) = A;

      deffunc F( Element of ( PFuncs (A,A))) = ( union { (($1 . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A });

      

       A1: ex a be Element of ( PFuncs (A,A)) st P[a]

      proof

        reconsider e = ( id A) as Element of ( PFuncs (A,A)) by PARTFUN1: 45;

        take e;

        thus thesis;

      end;

      

       A2: { {} where f be Element of ( PFuncs (A,A)) : P[f] } = { {} } from LATTICE3:sch 1( A1);

      assume

       A3: A = {} ;

      now

        let f be Element of ( PFuncs (A,A));

         not ex x be object st x in { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A }

        proof

          given x be object such that

           A4: x in { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A };

          ex x1 be Element of ( PFuncs (V,C)) st x = ((f . x1) \ x1) & x1 in A by A4;

          hence contradiction by A3;

        end;

        hence { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in A } = {} by XBOOLE_0:def 1;

      end;

      then

       A5: for v be Element of ( PFuncs (A,A)) st P[v] holds F(v) = G(v) by ZFMISC_1: 2;

      

       A6: { F(f) where f be Element of ( PFuncs (A,A)) : P[f] } = { G(f) where f be Element of ( PFuncs (A,A)) : P[f] } from FRAENKEL:sch 6( A5);

       {} 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;

      hence thesis by A6, A2, XBOOLE_1: 28;

    end;

    reserve u,v for Element of ( SubstLatt (V,C));

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

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

    

     Lm4: for X be set st X c= K holds X in ( SubstitutionSet (V,C))

    proof

      let X be set;

      assume

       A1: X c= K;

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

      then X c= ( PFuncs (V,C)) by A1;

      then

      reconsider B = X as Element of ( Fin ( PFuncs (V,C))) by A1, FINSUB_1:def 5;

      

       A2: for a, b st a in B & b in B & a c= b holds a = b by A1, SUBSTLAT: 5;

      for x be set st x in X holds x is finite by A1, Th1;

      then X in { 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) } by A2;

      hence thesis by SUBSTLAT:def 1;

    end;

    theorem :: HEYTING2:17

    

     Th17: for X be set st X c= u holds X is Element of ( SubstLatt (V,C))

    proof

      let X be set;

      reconsider u9 = u as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

      assume X c= u;

      then X c= u9;

      then X in ( SubstitutionSet (V,C)) by Lm4;

      hence thesis by SUBSTLAT:def 4;

    end;

    begin

    definition

      let V, C;

      :: HEYTING2:def4

      func pseudo_compl (V,C) -> UnOp of the carrier of ( SubstLatt (V,C)) means

      : Def4: for u9 be Element of ( SubstitutionSet (V,C)) st u9 = u holds (it . u) = ( mi ( - u9));

      existence

      proof

        deffunc F( Element of ( SubstitutionSet (V,C))) = ( mi ( - $1));

        consider IT be Function of ( SubstitutionSet (V,C)), ( SubstitutionSet (V,C)) such that

         A1: for u be Element of ( SubstitutionSet (V,C)) holds (IT . u) = F(u) from FUNCT_2:sch 4;

        ( SubstitutionSet (V,C)) = the carrier of ( SubstLatt (V,C)) by SUBSTLAT:def 4;

        then

        reconsider IT as UnOp of the carrier of ( SubstLatt (V,C));

        take IT;

        thus thesis by A1;

      end;

      correctness

      proof

        let IT,IT9 be UnOp of the carrier of ( SubstLatt (V,C));

        assume that

         A2: for u9 be Element of ( SubstitutionSet (V,C)) st u9 = u holds (IT . u) = ( mi ( - u9)) and

         A3: for u9 be Element of ( SubstitutionSet (V,C)) st u9 = u holds (IT9 . u) = ( mi ( - u9));

        now

          let u;

          reconsider u9 = u as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

          

          thus (IT . u) = ( mi ( - u9)) by A2

          .= (IT9 . u) by A3;

        end;

        hence IT = IT9 by FUNCT_2: 63;

      end;

      :: HEYTING2:def5

      func StrongImpl (V,C) -> BinOp of the carrier of ( SubstLatt (V,C)) means

      : Def5: for u9,v9 be Element of ( SubstitutionSet (V,C)) st u9 = u & v9 = v holds (it . (u,v)) = ( mi (u9 =>> v9));

      existence

      proof

        set ZA = the carrier of ( SubstLatt (V,C));

        defpred P[ set, set, set] means for u9,v9 be Element of ( SubstitutionSet (V,C)) st u9 = $1 & v9 = $2 holds $3 = ( mi (u9 =>> v9));

        

         A4: for x,y be Element of ZA holds ex z be Element of ZA st P[x, y, z]

        proof

          let x,y be Element of ZA;

          reconsider x9 = x, y9 = y as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

          reconsider z = ( mi (x9 =>> y9)) as Element of ZA by SUBSTLAT:def 4;

          take z;

          let u9,v9 be Element of ( SubstitutionSet (V,C));

          assume that

           A5: u9 = x and

           A6: v9 = y;

          thus thesis by A5, A6;

        end;

        consider o be BinOp of the carrier of ( SubstLatt (V,C)) such that

         A7: for a,b be Element of ( SubstLatt (V,C)) holds P[a, b, (o . (a,b))] from BINOP_1:sch 3( A4);

        take o;

        let u, v;

        let u9,v9 be Element of ( SubstitutionSet (V,C));

        assume that

         A8: u9 = u and

         A9: v9 = v;

        thus thesis by A7, A8, A9;

      end;

      correctness

      proof

        let IT1,IT2 be BinOp of the carrier of ( SubstLatt (V,C));

        assume that

         A10: for u9,v9 be Element of ( SubstitutionSet (V,C)) st u9 = u & v9 = v holds (IT1 . (u,v)) = ( mi (u9 =>> v9)) and

         A11: for u9,v9 be Element of ( SubstitutionSet (V,C)) st u9 = u & v9 = v holds (IT2 . (u,v)) = ( mi (u9 =>> v9));

        now

          let u, v;

          reconsider u9 = u, v9 = v as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

          

          thus (IT1 . (u,v)) = ( mi (u9 =>> v9)) by A10

          .= (IT2 . (u,v)) by A11;

        end;

        hence IT1 = IT2 by BINOP_1: 2;

      end;

      let u;

      :: HEYTING2:def6

      func SUB u -> Element of ( Fin the carrier of ( SubstLatt (V,C))) equals ( bool u);

      coherence

      proof

        reconsider u9 = u as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

        

         A12: ( bool u) c= the carrier of ( SubstLatt (V,C))

        proof

          let x be object;

          assume x in ( bool u);

          then x is Element of ( SubstLatt (V,C)) by Th17;

          hence thesis;

        end;

        u9 is finite;

        hence thesis by A12, FINSUB_1:def 5;

      end;

      correctness ;

      :: HEYTING2:def7

      func diff (u) -> UnOp of the carrier of ( SubstLatt (V,C)) means

      : Def7: (it . v) = (u \ v);

      existence

      proof

        deffunc F( set) = (u \ $1);

        consider IT be Function such that

         A13: ( dom IT) = the carrier of ( SubstLatt (V,C)) & for v be set st v in the carrier of ( SubstLatt (V,C)) holds (IT . v) = F(v) from FUNCT_1:sch 5;

        u in the carrier of ( SubstLatt (V,C));

        then

         A14: u in ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

        for x be object st x in the carrier of ( SubstLatt (V,C)) holds (IT . x) in ( Fin ( PFuncs (V,C)))

        proof

          let x be object;

          assume

           A15: x in the carrier of ( SubstLatt (V,C));

          reconsider x as set by TARSKI: 1;

          

           A16: (IT . x) = (u \ x) by A13, A15;

          (u \ x) in ( SubstitutionSet (V,C)) by A14, Lm4;

          hence thesis by A16;

        end;

        then

        reconsider IT as Function of the carrier of ( SubstLatt (V,C)), ( Fin ( PFuncs (V,C))) by A13, FUNCT_2: 3;

        now

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

          (u \ v) in ( SubstitutionSet (V,C)) by A14, Lm4;

          then (IT . v) in ( SubstitutionSet (V,C)) by A13;

          hence (IT . v) in the carrier of ( SubstLatt (V,C)) by SUBSTLAT:def 4;

        end;

        then

        reconsider IT as UnOp of the carrier of ( SubstLatt (V,C)) by HEYTING1: 1;

        take IT;

        let v;

        thus thesis by A13;

      end;

      correctness

      proof

        let IT,IT9 be UnOp of the carrier of ( SubstLatt (V,C));

        assume that

         A17: (IT . v) = (u \ v) and

         A18: (IT9 . v) = (u \ v);

        now

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

          

          thus (IT . v) = (u \ v) by A17

          .= (IT9 . v) by A18;

        end;

        hence IT = IT9 by FUNCT_2: 63;

      end;

    end

    

     Lm5: v in ( SUB u) implies (v "\/" (( diff u) . v)) = u

    proof

      assume

       A1: v in ( SUB u);

      reconsider u9 = u, v9 = v, dv = (( diff u) . v) as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

      

       A2: (u \ v) = (( diff u) . v) by Def7;

      

      thus (v "\/" (( diff u) . v)) = (the L_join of ( SubstLatt (V,C)) . (v,(( diff u) . v))) by LATTICES:def 1

      .= ( mi (v9 \/ dv)) by SUBSTLAT:def 4

      .= ( mi u9) by A1, A2, XBOOLE_1: 45

      .= u by SUBSTLAT: 11;

    end;

    

     Lm6: for K be Element of ( Fin ( PFuncs (V,C))) st K = {a} holds ex v be Element of ( SubstitutionSet (V,C)) st v in ( SUB u) & (v ^ K) = {} & for b st b in (( diff u) . v) holds b tolerates a

    proof

      deffunc F( set) = $1;

      let K be Element of ( Fin ( PFuncs (V,C))) such that

       A1: K = {a};

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

      defpred Q[ Element of ( PFuncs (V,C))] means not $1 tolerates a & $1 in u & $1 tolerates a;

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

      defpred P[ Element of ( PFuncs (V,C))] means $1 is finite & not $1 tolerates a;

      set M = { F(s) where s be Element of ( PFuncs (V,C)) : F(s) in u & P[s] };

      defpred P[ Element of ( PFuncs (V,C)), Element of ( PFuncs (V,C))] means $1 in M & $2 in {a} & $1 tolerates $2;

      defpred Q[ Element of ( PFuncs (V,C)), Element of ( PFuncs (V,C))] means $2 = a & $1 in M & $1 tolerates $2;

      defpred P[ Element of ( PFuncs (V,C))] means $1 in M & $1 tolerates a;

      defpred P1[ Element of ( PFuncs (V,C)), Element of ( PFuncs (V,C))] means $1 in M & $1 tolerates $2;

      deffunc F( Element of ( PFuncs (V,C))) = ($1 \/ a);

      

       A2: M c= u from FRAENKEL:sch 17;

      then

      reconsider v = M as Element of ( SubstLatt (V,C)) by Th17;

      reconsider v as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

      take v;

      thus v in ( SUB u) by A2;

      

       A3: P[s, t] iff Q[s, t] by TARSKI:def 1;

      

       A4: { F(s,t) : P[s, t] } = { F(s9,t9) where s9,t9 be Element of ( PFuncs (V,C)) : Q[s9, t9] } from FRAENKEL:sch 4( A3);

      s in M iff s is finite & not s tolerates a & s in u

      proof

        thus s in M implies s is finite & not s tolerates a & s in u

        proof

          assume s in M;

          then ex s2 be Element of ( PFuncs (V,C)) st s2 = s & s2 in u & s2 is finite & not s2 tolerates a;

          hence thesis;

        end;

        thus thesis;

      end;

      then

       A5: P[s] iff Q[s];

      

       A6: { F(s9) where s9 be Element of ( PFuncs (V,C)) : P[s9] } = { F(s) : Q[s] } from FRAENKEL:sch 3( A5);

      { F1(s,t) where t be Element of ( PFuncs (V,C)) : t = a & P1[s, t] } = { F1(s9,a) where s9 be Element of ( PFuncs (V,C)) : P1[s9, a] } from FRAENKEL:sch 20;

      then

       A7: (v ^ K) = { (s \/ a) : not s tolerates a & s in u & s tolerates a } by A1, A4, A6, SUBSTLAT:def 3;

      thus (v ^ K) = {}

      proof

        assume (v ^ K) <> {} ;

        then

        consider x be object such that

         A8: x in (v ^ K) by XBOOLE_0:def 1;

        ex s1 be Element of ( PFuncs (V,C)) st x = (s1 \/ a) & ( not s1 tolerates a) & s1 in u & s1 tolerates a by A7, A8;

        hence thesis;

      end;

      let b;

      assume b in (( diff u) . v);

      then

       A9: b in (u \ v) by Def7;

      then

       A10: not b in M by XBOOLE_0:def 5;

      u in the carrier of ( SubstLatt (V,C));

      then u in ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

      then b is finite by A9, Th1;

      hence thesis by A9, A10;

    end;

    definition

      let V, C;

      :: HEYTING2:def8

      func Atom (V,C) -> Function of ( PFuncs (V,C)), the carrier of ( SubstLatt (V,C)) means

      : Def8: for a be Element of ( PFuncs (V,C)) holds (it . a) = ( mi {.a.});

      existence

      proof

        deffunc F( Element of ( PFuncs (V,C))) = ( mi {.$1.});

        consider f be Function of ( PFuncs (V,C)), ( SubstitutionSet (V,C)) such that

         A1: for a be Element of ( PFuncs (V,C)) holds (f . a) = F(a) from FUNCT_2:sch 4;

        

         A2: the carrier of ( SubstLatt (V,C)) = ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

         A3:

        now

          let x be object;

          assume x in ( PFuncs (V,C));

          then

          reconsider a = x as Element of ( PFuncs (V,C));

          (f . a) = ( mi {.a.}) by A1;

          hence (f . x) in the carrier of ( SubstLatt (V,C)) by A2;

        end;

        ( dom f) = ( PFuncs (V,C)) by FUNCT_2:def 1;

        then

        reconsider f as Function of ( PFuncs (V,C)), the carrier of ( SubstLatt (V,C)) by A3, FUNCT_2: 3;

        take f;

        thus thesis by A1;

      end;

      correctness

      proof

        let IT1,IT2 be Function of ( PFuncs (V,C)), the carrier of ( SubstLatt (V,C)) such that

         A4: for a holds (IT1 . a) = ( mi {.a.}) and

         A5: for a holds (IT2 . a) = ( mi {.a.});

        now

          let a;

          (IT1 . a) = ( mi {.a.}) by A4;

          hence (IT1 . a) = (IT2 . a) by A5;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    

     Lm7: for a be Element of ( PFuncs (V,C)) st a is finite holds (( Atom (V,C)) . a) = {a}

    proof

      let a be Element of ( PFuncs (V,C));

      

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

      proof

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

        assume that

         A2: s in {a} and

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

        s = a by A2, TARSKI:def 1;

        hence thesis by A3, TARSKI:def 1;

      end;

      assume a is finite;

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

      then {.a.} in { 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) } by A1;

      then {a} in ( SubstitutionSet (V,C)) by SUBSTLAT:def 1;

      

      then {a} = ( mi {.a.}) by SUBSTLAT: 11

      .= (( Atom (V,C)) . a) by Def8;

      hence thesis;

    end;

    theorem :: HEYTING2:18

    

     Th18: ( FinJoin (K,( Atom (V,C)))) = ( FinUnion (K,( singleton ( PFuncs (V,C)))))

    proof

      deffunc F( Element of ( Fin ( PFuncs (V,C)))) = ( mi $1);

      

       A1: ( FinUnion (K,( singleton ( PFuncs (V,C))))) c= ( mi ( FinUnion (K,( singleton ( PFuncs (V,C))))))

      proof

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        assume

         A2: a in ( FinUnion (K,( singleton ( PFuncs (V,C)))));

        then

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

         A3: b in K and

         A4: a in (( singleton ( PFuncs (V,C))) . b) by SETWISEO: 57;

        

         A5: a = b by A4, SETWISEO: 55;

         A6:

        now

          K in ( SubstitutionSet (V,C));

          then K in { 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) } by SUBSTLAT:def 1;

          then

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

          let s be finite set;

          assume that

           A8: s in ( FinUnion (K,( singleton ( PFuncs (V,C))))) and

           A9: s c= aa;

          consider t such that

           A10: t in K and

           A11: s in (( singleton ( PFuncs (V,C))) . t) by A8, SETWISEO: 57;

          s = t by A11, SETWISEO: 55;

          hence s = a by A3, A5, A9, A10, A7;

        end;

        aa is finite by A3, A5, Th1;

        hence thesis by A2, A6, SUBSTLAT: 7;

      end;

      consider g be Function of ( Fin ( PFuncs (V,C))), ( SubstitutionSet (V,C)) such that

       A12: for B be Element of ( Fin ( PFuncs (V,C))) holds (g . B) = F(B) from FUNCT_2:sch 4;

      reconsider g as Function of ( Fin ( PFuncs (V,C))), the carrier of ( SubstLatt (V,C)) by SUBSTLAT:def 4;

       A13:

      now

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

        

         A14: (g . x) = ( mi x) by A12;

        

         A15: (g . y) = ( mi y) by A12;

        

        thus (g . (x \/ y)) = ( mi (x \/ y)) by A12

        .= ( mi (( mi x) \/ y)) by SUBSTLAT: 13

        .= ( mi (( mi x) \/ ( mi y))) by SUBSTLAT: 13

        .= (the L_join of ( SubstLatt (V,C)) . ((g . x),(g . y))) by A14, A15, SUBSTLAT:def 4;

      end;

       A16:

      now

        let a be object;

        assume

         A17: a in K;

        then

        reconsider a9 = a as Element of ( PFuncs (V,C)) by SETWISEO: 9;

        

         A18: a9 is finite by A17, Th1;

        then

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

        

        thus (((g * ( singleton ( PFuncs (V,C)))) | K) . a) = ((g * ( singleton ( PFuncs (V,C)))) . a) by A17, FUNCT_1: 49

        .= (g . (( singleton ( PFuncs (V,C))) . a9)) by FUNCT_2: 15

        .= (g . {a}) by SETWISEO: 54

        .= ( mi KL) by A12

        .= KL by SUBSTLAT: 11

        .= (( Atom (V,C)) . a9) by A18, Lm7

        .= ((( Atom (V,C)) | K) . a) by A17, FUNCT_1: 49;

      end;

      

       A19: ( mi ( FinUnion (K,( singleton ( PFuncs (V,C)))))) c= ( FinUnion (K,( singleton ( PFuncs (V,C))))) by SUBSTLAT: 8;

      

       A20: ( rng ( singleton ( PFuncs (V,C)))) c= ( Fin ( PFuncs (V,C)));

      

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

      then K c= ( dom ( Atom (V,C))) by FUNCT_2:def 1;

      then

       A22: ( dom (( Atom (V,C)) | K)) = K by RELAT_1: 62;

      reconsider gs = (g * ( singleton ( PFuncs (V,C)))) as Function of ( PFuncs (V,C)), the carrier of ( SubstLatt (V,C));

      

       A23: (g . ( {}. ( PFuncs (V,C)))) = ( mi ( {}. ( PFuncs (V,C)))) by A12

      .= {} by SUBSTLAT: 9

      .= ( Bottom ( SubstLatt (V,C))) by SUBSTLAT: 26

      .= ( the_unity_wrt the L_join of ( SubstLatt (V,C))) by LATTICE2: 18;

      ( dom g) = ( Fin ( PFuncs (V,C))) by FUNCT_2:def 1;

      then

       A24: ( dom (g * ( singleton ( PFuncs (V,C))))) = ( dom ( singleton ( PFuncs (V,C)))) by A20, RELAT_1: 27;

      ( dom ( singleton ( PFuncs (V,C)))) = ( PFuncs (V,C)) by FUNCT_2:def 1;

      then ( dom ((g * ( singleton ( PFuncs (V,C)))) | K)) = K by A21, A24, RELAT_1: 62;

      

      hence ( FinJoin (K,( Atom (V,C)))) = ( FinJoin (K,gs)) by A22, A16, FUNCT_1: 2, LATTICE2: 53

      .= (the L_join of ( SubstLatt (V,C)) $$ (K,gs)) by LATTICE2:def 3

      .= (g . ( FinUnion (K,( singleton ( PFuncs (V,C)))))) by A23, A13, SETWISEO: 53

      .= ( mi ( FinUnion (K,( singleton ( PFuncs (V,C)))))) by A12

      .= ( FinUnion (K,( singleton ( PFuncs (V,C))))) by A19, A1;

    end;

    theorem :: HEYTING2:19

    

     Th19: for u be Element of ( SubstitutionSet (V,C)) holds u = ( FinJoin (u,( Atom (V,C))))

    proof

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

      

      thus u = ( FinUnion (u,( singleton ( PFuncs (V,C))))) by SETWISEO: 58

      .= ( FinJoin (u,( Atom (V,C)))) by Th18;

    end;

    

     Lm8: (for a be set st a in u holds ex b be set st b in v & b c= a) implies u [= v

    proof

      assume

       A1: for a be set st a in u holds ex b be set st b in v & b c= a;

      reconsider u9 = u, v9 = v as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

      (u "/\" v) = (the L_meet of ( SubstLatt (V,C)) . (u9,v9)) by LATTICES:def 2

      .= ( mi (u9 ^ v9)) by SUBSTLAT:def 4

      .= u9 by A1, Th5;

      hence thesis by LATTICES: 4;

    end;

    theorem :: HEYTING2:20

    

     Th20: (( diff u) . v) [= u

    proof

      (( diff u) . v) = (u \ v) by Def7;

      then for a be set st a in (( diff u) . v) holds ex b be set st b in u & b c= a;

      hence thesis by Lm8;

    end;

    theorem :: HEYTING2:21

    

     Th21: for a be Element of ( PFuncs (V,C)) st a is finite holds for c be set st c in (( Atom (V,C)) . a) holds c = a

    proof

      let a be Element of ( PFuncs (V,C));

      assume a is finite;

      then (( Atom (V,C)) . a) = {a} by Lm7;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: HEYTING2:22

    

     Th22: for a be Element of ( PFuncs (V,C)) st K = {a} & L = u & (L ^ K) = {} holds (( Atom (V,C)) . a) [= (( pseudo_compl (V,C)) . u)

    proof

      let a be Element of ( PFuncs (V,C));

      assume that

       A1: K = {a} and

       A2: L = u and

       A3: (L ^ K) = {} ;

      a in K by A1, TARSKI:def 1;

      then

       A4: a is finite by Th1;

      now

        let c be set;

        assume

         A5: c in (( Atom (V,C)) . a);

        then

        reconsider c9 = c as Element of ( PFuncs (V,C)) by A4, Th21;

        c = a by A4, A5, Th21;

        then

        consider b be finite set such that

         A6: b in ( - L) and

         A7: b c= c9 by A1, A3, Th14;

        consider d be set such that

         A8: d c= b and

         A9: d in ( mi ( - L)) by A6, SUBSTLAT: 10;

        take e = d;

        thus e in (( pseudo_compl (V,C)) . u) by A2, A9, Def4;

        thus e c= c by A7, A8;

      end;

      hence thesis by Lm8;

    end;

    theorem :: HEYTING2:23

    

     Th23: for a be finite Element of ( PFuncs (V,C)) holds a in (( Atom (V,C)) . a)

    proof

      let a be finite Element of ( PFuncs (V,C));

      (( Atom (V,C)) . a) = {a} by Lm7;

      hence thesis by TARSKI:def 1;

    end;

    

     Lm9: u [= v implies for x be set st x in u holds ex b be set st b in v & b c= x

    proof

      reconsider u9 = u, v9 = v as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

      assume u [= v;

      

      then u = (u "/\" v) by LATTICES: 4

      .= (the L_meet of ( SubstLatt (V,C)) . (u,v)) by LATTICES:def 2

      .= ( mi (u9 ^ v9)) by SUBSTLAT:def 4;

      hence thesis by Th4;

    end;

    theorem :: HEYTING2:24

    

     Th24: for u,v be Element of ( SubstitutionSet (V,C)) holds ((for c be set st c in u holds ex b be set st b in v & b c= (c \/ a)) implies ex b be set st b in (u =>> v) & b c= a)

    proof

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

      reconsider u9 = u as Element of ( SubstLatt (V,C)) by SUBSTLAT:def 4;

      defpred P[ set, set] means $2 in v & $2 c= ($1 \/ a);

      assume that

       A1: for b be set st b in u holds ex c be set st c in v & c c= (b \/ a);

       A2:

      now

        let b be Element of ( PFuncs (V,C));

        assume b in u;

        then

        consider c be set such that

         A3: c in v and

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

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

        then

        reconsider c as Element of ( PFuncs (V,C)) by A3;

        take x = c;

        thus P[b, x] by A3, A4;

      end;

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

       A5: b in u implies P[b, (f9 . b)] from FRAENKEL:sch 27( A2);

      set g = (f9 | u);

      consider f2 be Function such that

       A6: f9 = f2 and ( dom f2) = ( PFuncs (V,C)) and ( rng f2) c= ( PFuncs (V,C)) by FUNCT_2:def 2;

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

      then g is Function of u, ( PFuncs (V,C)) by FUNCT_2: 32;

      then

       A7: ( dom g) = u by FUNCT_2:def 1;

      for b be object st b in u holds (g . b) in v

      proof

        let b be object;

        assume

         A8: b in u;

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

        then

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

        (g . b9) = (f2 . b9) by A6, A8, FUNCT_1: 49;

        hence thesis by A5, A6, A8;

      end;

      then g is Function of u, v by A7, FUNCT_2: 3;

      then

       A9: ( rng g) c= v by RELAT_1:def 19;

      

       A10: for b be set st b in u9 holds (g . b) c= (b \/ a)

      proof

        let b be set;

        assume

         A11: b in u9;

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

        then

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

        (g . b9) = (f2 . b9) by A6, A11, FUNCT_1: 49;

        hence thesis by A5, A6, A11;

      end;

      reconsider g as Element of ( PFuncs (u,v)) by A7, A9, PARTFUN1:def 3;

      set d = ( union { ((g . i) \ i) where i be Element of ( PFuncs (V,C)) : i in u9 });

      

       A12: d c= a

      proof

        let x be object;

        assume x in d;

        then

        consider Y be set such that

         A13: x in Y and

         A14: Y in { ((g . i) \ i) where i be Element of ( PFuncs (V,C)) : i in u9 } by TARSKI:def 4;

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

         A15: Y = ((g . j) \ j) and

         A16: j in u9 by A14;

        (g . j) c= (j \/ a) by A10, A16;

        then ((g . j) \ j) c= a by XBOOLE_1: 43;

        hence thesis by A13, A15;

      end;

      then

      reconsider d as Element of ( PFuncs (V,C)) by PRE_POLY: 15;

      take d;

      d in { ( union { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in u }) where f be Element of ( PFuncs (u,v)) : ( dom f) = u } by A7;

      hence d in (u =>> v) by XBOOLE_0:def 4;

      thus thesis by A12;

    end;

    theorem :: HEYTING2:25

    

     Th25: for a be finite Element of ( PFuncs (V,C)) st (for b be Element of ( PFuncs (V,C)) st b in u holds b tolerates a) & (u "/\" (( Atom (V,C)) . a)) [= v holds (( Atom (V,C)) . a) [= (( StrongImpl (V,C)) . (u,v))

    proof

      let a be finite Element of ( PFuncs (V,C));

      assume that

       A1: for b be Element of ( PFuncs (V,C)) st b in u holds b tolerates a and

       A2: (u "/\" (( Atom (V,C)) . a)) [= v;

      reconsider u9 = u, v9 = v, Aa = (( Atom (V,C)) . a) as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

       A3:

      now

        let c be set;

        

         A4: a in Aa by Th23;

        assume

         A5: c in u;

        then

         A6: c in u9;

        then

        reconsider c9 = c as Element of ( PFuncs (V,C)) by SETWISEO: 9;

        c9 tolerates a by A1, A5;

        then (c \/ a) in { (s1 \/ t1) where s1,t1 be Element of ( PFuncs (V,C)) : s1 in u9 & t1 in Aa & s1 tolerates t1 } by A5, A4;

        then

         A7: (c \/ a) in (u9 ^ Aa) by SUBSTLAT:def 3;

        c is finite by A6, Th1;

        then

        consider b be set such that

         A8: b c= (c \/ a) and

         A9: b in ( mi (u9 ^ Aa)) by A7, SUBSTLAT: 10;

        b in (the L_meet of ( SubstLatt (V,C)) . (u,(( Atom (V,C)) . a))) by A9, SUBSTLAT:def 4;

        then b in (u "/\" (( Atom (V,C)) . a)) by LATTICES:def 2;

        then

        consider d be set such that

         A10: d in v and

         A11: d c= b by A2, Lm9;

        take e = d;

        thus e in v by A10;

        thus e c= (c \/ a) by A8, A11;

      end;

      now

        let c be set;

        assume

         A12: c in (( Atom (V,C)) . a);

        then c = a by Th21;

        then

        consider b be set such that

         A13: b in (u9 =>> v9) and

         A14: b c= c by A3, Th24;

        c in Aa by A12;

        then c is finite by Th1;

        then

        consider d be set such that

         A15: d c= b and

         A16: d in ( mi (u9 =>> v9)) by A13, A14, SUBSTLAT: 10;

        take e = d;

        thus e in (( StrongImpl (V,C)) . (u,v)) by A16, Def5;

        thus e c= c by A14, A15;

      end;

      hence thesis by Lm8;

    end;

    deffunc M( set, set) = the L_meet of ( SubstLatt ($1,$2));

    theorem :: HEYTING2:26

    

     Th26: (u "/\" (( pseudo_compl (V,C)) . u)) = ( Bottom ( SubstLatt (V,C)))

    proof

      reconsider u9 = u as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

      

      thus (u "/\" (( pseudo_compl (V,C)) . u)) = ( M(V,C) . (u,(( pseudo_compl (V,C)) . u))) by LATTICES:def 2

      .= ( M(V,C) . (u,( mi ( - u9)))) by Def4

      .= ( mi (u9 ^ ( mi ( - u9)))) by SUBSTLAT:def 4

      .= ( mi (u9 ^ ( - u9))) by SUBSTLAT: 20

      .= ( Bottom ( SubstLatt (V,C))) by Th12;

    end;

    theorem :: HEYTING2:27

    

     Th27: (u "/\" (( StrongImpl (V,C)) . (u,v))) [= v

    proof

      now

        reconsider u9 = u, v9 = v as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

        let a be set;

        assume

         A1: a in (u "/\" (( StrongImpl (V,C)) . (u,v)));

        (u "/\" (( StrongImpl (V,C)) . (u,v))) = ( M(V,C) . (u,(( StrongImpl (V,C)) . (u,v)))) by LATTICES:def 2

        .= ( M(V,C) . (u,( mi (u9 =>> v9)))) by Def5

        .= ( mi (u9 ^ ( mi (u9 =>> v9)))) by SUBSTLAT:def 4

        .= ( mi (u9 ^ (u9 =>> v9))) by SUBSTLAT: 20;

        then a in (u9 ^ (u9 =>> v9)) by A1, SUBSTLAT: 6;

        hence ex b be set st b in v & b c= a by Lm3;

      end;

      hence thesis by Lm8;

    end;

     Lm10:

    now

      let V, C, u, v;

      deffunc IMPL( Element of ( SubstLatt (V,C)), Element of ( SubstLatt (V,C))) = ( FinJoin (( SUB $1),( M(V,C) .: (( pseudo_compl (V,C)),(( StrongImpl (V,C)) [:] (( diff $1),$2))))));

      set Psi = ( M(V,C) .: (( pseudo_compl (V,C)),(( StrongImpl (V,C)) [:] (( diff u),v))));

      reconsider v9 = v as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

       A1:

      now

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

        set u2 = (( diff u) . w), pc = (( pseudo_compl (V,C)) . w), si = (( StrongImpl (V,C)) . (u2,v));

        

         A2: (w "/\" (pc "/\" si)) = ((w "/\" pc) "/\" si) by LATTICES:def 7

        .= (( Bottom ( SubstLatt (V,C))) "/\" si) by Th26

        .= ( Bottom ( SubstLatt (V,C)));

        assume w in ( SUB u);

        then

         A3: (w "\/" u2) = u by Lm5;

        (( M(V,C) [;] (u,Psi)) . w) = ( M(V,C) . (u,(Psi . w))) by FUNCOP_1: 53

        .= (u "/\" (Psi . w)) by LATTICES:def 2

        .= (u "/\" ( M(V,C) . (pc,((( StrongImpl (V,C)) [:] (( diff u),v)) . w)))) by FUNCOP_1: 37

        .= (u "/\" (pc "/\" ((( StrongImpl (V,C)) [:] (( diff u),v)) . w))) by LATTICES:def 2

        .= (u "/\" (pc "/\" si)) by FUNCOP_1: 48

        .= ((w "/\" (pc "/\" si)) "\/" (u2 "/\" (pc "/\" si))) by A3, LATTICES:def 11

        .= (u2 "/\" (si "/\" pc)) by A2

        .= ((u2 "/\" si) "/\" pc) by LATTICES:def 7;

        then

         A4: (( M(V,C) [;] (u,Psi)) . w) [= (u2 "/\" si) by LATTICES: 6;

        (u2 "/\" si) [= v by Th27;

        hence (( M(V,C) [;] (u,Psi)) . w) [= v by A4, LATTICES: 7;

      end;

      (u "/\" IMPL(u,v)) = ( FinJoin (( SUB u),( M(V,C) [;] (u,Psi)))) by LATTICE2: 66;

      hence (u "/\" IMPL(u,v)) [= v by A1, LATTICE2: 54;

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

      assume

       A5: (u "/\" v) [= w;

      

       A6: v = ( FinJoin (v9,( Atom (V,C)))) by Th19;

      then

       A7: (u "/\" v) = ( FinJoin (v9,( M(V,C) [;] (u,( Atom (V,C)))))) by LATTICE2: 66;

      now

        set pf = ( pseudo_compl (V,C)), sf = (( StrongImpl (V,C)) [:] (( diff u),w));

        let a be Element of ( PFuncs (V,C));

        reconsider SA = {.a.} as Element of ( Fin ( PFuncs (V,C)));

        consider v be Element of ( SubstitutionSet (V,C)) such that

         A8: v in ( SUB u) and

         A9: (v ^ SA) = {} and

         A10: for b be Element of ( PFuncs (V,C)) st b in (( diff u) . v) holds b tolerates a by Lm6;

        assume

         A11: a in v9;

        then

         A12: a is finite by Th1;

        reconsider v9 = v as Element of ( SubstLatt (V,C)) by SUBSTLAT:def 4;

        set dv = (( diff u) . v9);

        (( M(V,C) [;] (u,( Atom (V,C)))) . a) [= w by A7, A5, A11, LATTICE2: 31;

        then ( M(V,C) . (u,(( Atom (V,C)) . a))) [= w by FUNCOP_1: 53;

        then

         A13: (u "/\" (( Atom (V,C)) . a)) [= w by LATTICES:def 2;

        a is finite by A11, Th1;

        then

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

        (v ^ SS) = {} by A9;

        then

         A14: (( Atom (V,C)) . a) [= (pf . v9) by Th22;

        (dv "/\" (( Atom (V,C)) . a)) [= (u "/\" (( Atom (V,C)) . a)) by Th20, LATTICES: 9;

        then (dv "/\" (( Atom (V,C)) . a)) [= w by A13, LATTICES: 7;

        then (( Atom (V,C)) . a) [= (( StrongImpl (V,C)) . ((( diff u) . v9),w)) by A10, A12, Th25;

        then

         A15: (( Atom (V,C)) . a) [= (sf . v9) by FUNCOP_1: 48;

        ((pf . v9) "/\" (sf . v9)) = ( M(V,C) . ((pf . v9),(sf . v9))) by LATTICES:def 2

        .= (( M(V,C) .: (pf,sf)) . v9) by FUNCOP_1: 37;

        then (( Atom (V,C)) . a) [= (( M(V,C) .: (pf,sf)) . v9) by A14, A15, FILTER_0: 7;

        hence (( Atom (V,C)) . a) [= IMPL(u,w) by A8, LATTICE2: 29;

      end;

      hence v [= IMPL(u,w) by A6, LATTICE2: 54;

    end;

    

     Lm11: ( SubstLatt (V,C)) is implicative

    proof

      let p,q be Element of ( SubstLatt (V,C));

      take r = ( FinJoin (( SUB p),( M(V,C) .: (( pseudo_compl (V,C)),(( StrongImpl (V,C)) [:] (( diff p),q))))));

      thus (p "/\" r) [= q & for r1 be Element of ( SubstLatt (V,C)) st (p "/\" r1) [= q holds r1 [= r by Lm10;

    end;

    registration

      let V, C;

      cluster ( SubstLatt (V,C)) -> implicative;

      coherence by Lm11;

    end

    theorem :: HEYTING2:28

    (u => v) = ( FinJoin (( SUB u),(the L_meet of ( SubstLatt (V,C)) .: (( pseudo_compl (V,C)),(( StrongImpl (V,C)) [:] (( diff u),v))))))

    proof

      deffunc IMPL( Element of ( SubstLatt (V,C)), Element of ( SubstLatt (V,C))) = ( FinJoin (( SUB $1),( M(V,C) .: (( pseudo_compl (V,C)),(( StrongImpl (V,C)) [:] (( diff $1),$2))))));

      

       A1: for w be Element of ( SubstLatt (V,C)) st (u "/\" w) [= v holds w [= IMPL(u,v) by Lm10;

      (u "/\" IMPL(u,v)) [= v by Lm10;

      hence thesis by A1, FILTER_0:def 7;

    end;