heyting3.miz



    begin

    scheme :: HEYTING3:sch1

    SSubsetUniq { R() -> 1-sorted , P[ object] } :

for A1,A2 be Subset of R() st (for x be object holds x in A1 iff P[x]) & (for x be object holds x in A2 iff P[x]) holds A1 = A2;

      let A1,A2 be Subset of R();

      assume that

       A1: for x be object holds x in A1 iff P[x] and

       A2: for x be object holds x in A2 iff P[x];

      thus A1 c= A2 by A1, A2;

      let x be object;

      assume x in A2;

      then P[x] by A2;

      hence thesis by A1;

    end;

    

     Lm1: for A,x be set holds [:A, {x}:] is Function

    proof

      let A,x be set;

      set X = [:A, {x}:];

      X is Function-like

      proof

        let y,y1,y2 be object;

        assume that

         A1: [y, y1] in X and

         A2: [y, y2] in X;

        y1 = x by A1, ZFMISC_1: 106;

        hence thesis by A2, ZFMISC_1: 106;

      end;

      hence thesis;

    end;

    registration

      let A,x be set;

      cluster [:A, {x}:] -> Function-like;

      coherence by Lm1;

    end

    

     Lm2: 0 = (2 * 0 );

    

     Lm3: 1 = ( 0 + 1);

    theorem :: HEYTING3:1

    

     Th1: for X be finite non empty Subset of NAT holds ex n be Element of NAT st X c= (( Seg n) \/ { 0 })

    proof

      let X be finite non empty Subset of NAT ;

      reconsider m = ( max X) as Element of NAT by ORDINAL1:def 12;

      take m;

      let x be object;

      

       A1: ( Seg m) c= (( Seg m) \/ { 0 }) by XBOOLE_1: 7;

      

       A2: { 0 } c= (( Seg m) \/ { 0 }) by XBOOLE_1: 7;

      assume

       A3: x in X;

      then

      reconsider n = x as Element of NAT ;

      

       A4: n <= m by A3, XXREAL_2:def 8;

      per cases by NAT_1: 25;

        suppose 1 <= n;

        then n in ( Seg m) by A4, FINSEQ_1: 1;

        hence thesis by A1;

      end;

        suppose 0 = n;

        then n in { 0 } by TARSKI:def 1;

        hence thesis by A2;

      end;

    end;

    theorem :: HEYTING3:2

    for X be finite Subset of NAT holds ex k be odd Element of NAT st not k in X

    proof

      let X be finite Subset of NAT ;

      per cases ;

        suppose X is non empty;

        then

        consider n be Element of NAT such that

         A1: X c= (( Seg n) \/ { 0 }) by Th1;

        

         A2: not ((2 * n) + 1) in X

        proof

          

           A3: not ((2 * n) + 1) in { 0 } by TARSKI:def 1;

          assume ((2 * n) + 1) in X;

          then ((2 * n) + 1) in ( Seg n) by A1, A3, XBOOLE_0:def 3;

          then

           A4: ((2 * n) + 1) <= n by FINSEQ_1: 1;

          (1 * n) <= (2 * n) by NAT_1: 4;

          hence thesis by A4, NAT_1: 13;

        end;

        assume for k be odd Element of NAT holds k in X;

        hence contradiction by A2;

      end;

        suppose X is empty;

        hence thesis;

      end;

    end;

    theorem :: HEYTING3:3

    

     Th3: for k be Element of NAT , X be finite non empty Subset of [: NAT , {k}:] holds ex n be non zero Element of NAT st X c= [:(( Seg n) \/ { 0 }), {k}:]

    proof

      let k be Element of NAT ;

      let X be finite non empty Subset of [: NAT , {k}:];

      reconsider pX = ( proj1 X) as finite non empty Subset of NAT by FUNCT_5: 11;

      reconsider mpX = ( max pX) as Element of NAT by ORDINAL1:def 12;

      reconsider m = (mpX + 1) as non zero Element of NAT ;

      take m;

      let x be object;

      

       A1: ( Seg m) c= (( Seg m) \/ { 0 }) by XBOOLE_1: 7;

      

       A2: { 0 } c= (( Seg m) \/ { 0 }) by XBOOLE_1: 7;

      assume

       A3: x in X;

      then

      consider x1,x2 be object such that

       A4: x1 in NAT and

       A5: x2 in {k} and

       A6: x = [x1, x2] by ZFMISC_1:def 2;

      reconsider n = (x `1 ) as Element of NAT by A4, A6;

      n in pX by A3, A6, XTUPLE_0:def 12;

      then ( max pX) <= m & n <= ( max pX) by NAT_1: 11, XXREAL_2:def 8;

      then

       A7: n <= m by XXREAL_0: 2;

      per cases by NAT_1: 25;

        suppose 1 <= n;

        then n in ( Seg m) by A7, FINSEQ_1: 1;

        hence thesis by A5, A6, A1, ZFMISC_1: 87;

      end;

        suppose 0 = n;

        then n in { 0 } by TARSKI:def 1;

        hence thesis by A5, A6, A2, ZFMISC_1: 87;

      end;

    end;

    theorem :: HEYTING3:4

    

     Th4: for m be Element of NAT , X be finite non empty Subset of [: NAT , {m}:] holds ex k be non zero Element of NAT st not [((2 * k) + 1), m] in X

    proof

      let m be Element of NAT ;

      let X be finite non empty Subset of [: NAT , {m}:];

      consider n be non zero Element of NAT such that

       A1: X c= [:(( Seg n) \/ { 0 }), {m}:] by Th3;

      

       A2: not [((2 * n) + 1), m] in X

      proof

        assume [((2 * n) + 1), m] in X;

        then

         A3: ((2 * n) + 1) in (( Seg n) \/ { 0 }) by A1, ZFMISC_1: 87;

         not ((2 * n) + 1) in { 0 } by TARSKI:def 1;

        then ((2 * n) + 1) in ( Seg n) by A3, XBOOLE_0:def 3;

        then

         A4: ((2 * n) + 1) <= n by FINSEQ_1: 1;

        (1 * n) <= (2 * n) by NAT_1: 4;

        hence thesis by A4, NAT_1: 13;

      end;

      assume for k be non zero Element of NAT holds [((2 * k) + 1), m] in X;

      hence contradiction by A2;

    end;

    theorem :: HEYTING3:5

    for m be Element of NAT , X be finite Subset of [: NAT , {m}:] holds ex k be Element of NAT st for l be Element of NAT st l >= k holds not [l, m] in X

    proof

      let m be Element of NAT ;

      let X be finite Subset of [: NAT , {m}:];

      per cases ;

        suppose X is non empty;

        then

        reconsider X9 = X as finite non empty Subset of [: NAT , {m}:];

        consider n be non zero Element of NAT such that

         A1: X9 c= [:(( Seg n) \/ { 0 }), {m}:] by Th3;

        take k = (n + 1);

        let l be Element of NAT ;

        assume

         A2: l >= k;

        assume [l, m] in X;

        then

         A3: l in (( Seg n) \/ { 0 }) by A1, ZFMISC_1: 87;

        now

          per cases by A3, XBOOLE_0:def 3;

            suppose l in ( Seg n);

            then l <= n by FINSEQ_1: 1;

            hence contradiction by A2, NAT_1: 13;

          end;

            suppose l in { 0 };

            hence contradiction by A2, TARSKI:def 1;

          end;

        end;

        hence thesis;

      end;

        suppose X is empty;

        then for l be Element of NAT st l >= 0 holds not [l, m] in X;

        hence thesis;

      end;

    end;

    theorem :: HEYTING3:6

    for L be upper-bounded Lattice holds ( Top L) = ( Top ( LattPOSet L))

    proof

      let L be upper-bounded Lattice;

      set x = ( % ( Top ( LattPOSet L)));

      now

        let a be Element of L;

        (a % ) <= (x % ) by YELLOW_0: 45;

        then a [= x by LATTICE3: 7;

        hence (x "\/" a) = x & (a "\/" x) = x by LATTICES:def 3;

      end;

      hence thesis by LATTICES:def 17;

    end;

    theorem :: HEYTING3:7

    for L be lower-bounded Lattice holds ( Bottom L) = ( Bottom ( LattPOSet L))

    proof

      let L be lower-bounded Lattice;

      set x = ( % ( Bottom ( LattPOSet L)));

      now

        let a be Element of L;

        (a % ) >= (x % ) by YELLOW_0: 44;

        then x [= a by LATTICE3: 7;

        hence (x "/\" a) = x & (a "/\" x) = x by LATTICES: 4;

      end;

      hence thesis by LATTICES:def 16;

    end;

    begin

    theorem :: HEYTING3:8

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

    proof

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

      assume

       A1: A = {} & B <> {} ;

      assume (B =>> A) <> {} ;

      then

      consider k be object such that

       A2: k in (B =>> A) by XBOOLE_0:def 1;

      ex f be PartFunc of B, A st k = ( union { ((f . i) \ i) where i be Element of ( PFuncs (V,C)) : i in B }) & ( dom f) = B by A2, HEYTING2: 15;

      hence thesis by A1;

    end;

    theorem :: HEYTING3:9

    

     Th9: for V,V9,C,C9 be set st V c= V9 & C c= C9 holds ( SubstitutionSet (V,C)) c= ( SubstitutionSet (V9,C9))

    proof

      let V,V9,C,C9 be set;

      assume V c= V9 & C c= C9;

      then

       A1: ( PFuncs (V,C)) c= ( PFuncs (V9,C9)) by PARTFUN1: 50;

      let x be object;

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

      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 SUBSTLAT:def 1;

      then

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

       A2: B = x & for u be set st u in B holds u is finite and

       A3: for s,t be Element of ( PFuncs (V,C)) holds (s in B & t in B & s c= t implies s = t);

      

       A4: B in ( Fin ( PFuncs (V,C))) & ( Fin ( PFuncs (V,C))) c= ( Fin ( PFuncs (V9,C9))) by A1, FINSUB_1: 10;

      

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

      reconsider B as Element of ( Fin ( PFuncs (V9,C9))) by A4;

      for s,t be Element of ( PFuncs (V9,C9)) st s in B & t in B & s c= t holds s = t by A3, A5;

      then x in { D where D be Element of ( Fin ( PFuncs (V9,C9))) : (for u be set st u in D holds u is finite) & for s,t be Element of ( PFuncs (V9,C9)) holds (s in D & t in D & s c= t implies s = t) } by A2;

      hence thesis by SUBSTLAT:def 1;

    end;

    theorem :: HEYTING3:10

    

     Th10: for V,V9,C,C9 be set, A be Element of ( Fin ( PFuncs (V,C))), B be Element of ( Fin ( PFuncs (V9,C9))) st V c= V9 & C c= C9 & A = B holds ( mi A) = ( mi B)

    proof

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

      assume that

       A1: V c= V9 & C c= C9 and

       A2: A = B;

      hereby

        let x be object;

        

         A3: ( PFuncs (V,C)) c= ( PFuncs (V9,C9)) by A1, PARTFUN1: 50;

        assume

         A4: x in ( mi A);

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

        then

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

         A5: f = x and

         A6: f is finite and for s be Element of ( PFuncs (V,C)) holds (s in A & s c= f iff s = f);

        reconsider f as Element of ( PFuncs (V9,C9)) by A3;

        for s be Element of ( PFuncs (V9,C9)) holds s in B & s c= f iff s = f by A2, A4, A5, SUBSTLAT: 6;

        then x in { t where t be Element of ( PFuncs (V9,C9)) : t is finite & for s be Element of ( PFuncs (V9,C9)) holds (s in B & s c= t iff s = t) } by A5, A6;

        hence x in ( mi B) by SUBSTLAT:def 2;

      end;

      let x be object;

      assume

       A7: x in ( mi B);

      then x in { t where t be Element of ( PFuncs (V9,C9)) : t is finite & for s be Element of ( PFuncs (V9,C9)) holds (s in B & s c= t iff s = t) } by SUBSTLAT:def 2;

      then ex f be Element of ( PFuncs (V9,C9)) st f = x & f is finite & for s be Element of ( PFuncs (V9,C9)) holds (s in B & s c= f iff s = f);

      then

      reconsider x9 = x as finite set;

      ( mi B) c= B & for b be finite set st b in A & b c= x9 holds b = x9 by A2, A7, SUBSTLAT: 6;

      hence thesis by A2, A7, SUBSTLAT: 7;

    end;

    theorem :: HEYTING3:11

    for V,V9,C,C9 be set st V c= V9 & C c= C9 holds the L_join of ( SubstLatt (V,C)) = (the L_join of ( SubstLatt (V9,C9)) || the carrier of ( SubstLatt (V,C)))

    proof

      let V,V9,C,C9 be set;

      set K = ( SubstLatt (V,C)), L = ( SubstLatt (V9,C9));

      

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

      

       A2: ( dom the L_join of L) = [:the carrier of L, the carrier of L:] by FUNCT_2:def 1;

      reconsider B1 = the L_join of K as BinOp of the carrier of K;

      set B2 = (the L_join of L || the carrier of K);

      assume

       A3: V c= V9 & C c= C9;

      ( SubstitutionSet (V9,C9)) = the carrier of L by SUBSTLAT:def 4;

      then the carrier of K c= the carrier of L by A1, A3, Th9;

      then

       A4: ( dom B2) = [:the carrier of K, the carrier of K:] by A2, RELAT_1: 62, ZFMISC_1: 96;

      

       A5: ( SubstitutionSet (V,C)) c= ( SubstitutionSet (V9,C9)) by A3, Th9;

      ( rng B2) c= the carrier of K

      proof

        let x be object;

        assume x in ( rng B2);

        then

        consider y be object such that

         A6: y in ( dom B2) and

         A7: x = (B2 . y) by FUNCT_1:def 3;

        consider y1,y2 be object such that

         A8: y1 in the carrier of K & y2 in the carrier of K and

         A9: y = [y1, y2] by A4, A6, ZFMISC_1:def 2;

        y1 in ( SubstitutionSet (V,C)) & y2 in ( SubstitutionSet (V,C)) by A8, SUBSTLAT:def 4;

        then

        reconsider y19 = y1, y29 = y2 as Element of ( SubstitutionSet (V9,C9)) by A5;

        reconsider y11 = y1, y22 = y2 as Element of ( SubstitutionSet (V,C)) by A8, SUBSTLAT:def 4;

        (B2 . y) = (the L_join of L . (y1,y2)) by A4, A6, A9, FUNCT_1: 49

        .= ( mi (y19 \/ y29)) by SUBSTLAT:def 4

        .= ( mi (y11 \/ y22)) by A3, Th10;

        hence thesis by A1, A7;

      end;

      then

      reconsider B2 as BinOp of the carrier of K by A4, FUNCT_2: 2;

      now

        let a,b be Element of K;

        reconsider a9 = a, b9 = b as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

        a9 in ( SubstitutionSet (V,C)) & b9 in ( SubstitutionSet (V,C));

        then

        reconsider a1 = a, b1 = b as Element of ( SubstitutionSet (V9,C9)) by A5;

        

        thus (B1 . (a,b)) = ( mi (a9 \/ b9)) by SUBSTLAT:def 4

        .= ( mi (a1 \/ b1)) by A3, Th10

        .= (the L_join of L . (a,b)) by SUBSTLAT:def 4

        .= (B2 . [a, b]) by FUNCT_1: 49

        .= (B2 . (a,b));

      end;

      hence thesis by BINOP_1: 2;

    end;

    definition

      let V,C be set;

      :: HEYTING3:def1

      func SubstPoset (V,C) -> RelStr equals ( LattPOSet ( SubstLatt (V,C)));

      coherence ;

    end

    registration

      let V,C be set;

      cluster ( SubstPoset (V,C)) -> with_suprema with_infima;

      coherence ;

    end

    registration

      let V,C be set;

      cluster ( SubstPoset (V,C)) -> reflexive antisymmetric transitive;

      coherence ;

    end

    theorem :: HEYTING3:12

    

     Th12: for V,C be set, a,b be Element of ( SubstPoset (V,C)) holds a <= b iff for x be set st x in a holds ex y be set st y in b & y c= x

    proof

      let V,C be set;

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

      reconsider a9 = a, b9 = b as Element of ( SubstLatt (V,C));

      reconsider a1 = a, b1 = b as Element of ( SubstitutionSet (V,C)) by SUBSTLAT:def 4;

      

       A1: (a9 % ) = a & (b9 % ) = b;

      hereby

        assume a <= b;

        then a9 [= b9 by A1, LATTICE3: 7;

        

        then a9 = (a9 "/\" b9) by LATTICES: 4

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

        .= ( mi (a1 ^ b1)) by SUBSTLAT:def 4;

        hence for x be set st x in a holds ex y be set st y in b & y c= x by HEYTING2: 4;

      end;

      assume for x be set st x in a holds ex y be set st y in b & y c= x;

      then ( mi (a1 ^ b1)) = a1 by HEYTING2: 5;

      

      then a9 = (the L_meet of ( SubstLatt (V,C)) . (a9,b9)) by SUBSTLAT:def 4

      .= (a9 "/\" b9) by LATTICES:def 2;

      then a9 [= b9 by LATTICES: 4;

      hence thesis by A1, LATTICE3: 7;

    end;

    theorem :: HEYTING3:13

    for V,V9,C,C9 be set st V c= V9 & C c= C9 holds ( SubstPoset (V,C)) is full SubRelStr of ( SubstPoset (V9,C9))

    proof

      let V,V9,C,C9 be set;

      set K = ( SubstPoset (V,C)), L = ( SubstPoset (V9,C9));

      

       A1: the carrier of K = ( SubstitutionSet (V,C)) & the carrier of L = ( SubstitutionSet (V9,C9)) by SUBSTLAT:def 4;

      assume V c= V9 & C c= C9;

      then

       A2: the carrier of K c= the carrier of L by A1, Th9;

      now

        let a,b be object;

        assume

         A3: [a, b] in the InternalRel of K;

        then

        reconsider a9 = a, b9 = b as Element of K by ZFMISC_1: 87;

        a in the carrier of K & b in the carrier of K by A3, ZFMISC_1: 87;

        then

        reconsider a1 = a, b1 = b as Element of L by A2;

        a9 <= b9 by A3, ORDERS_2:def 5;

        then for x be set st x in a9 holds ex y be set st y in b9 & y c= x by Th12;

        then a1 <= b1 by Th12;

        hence [a, b] in the InternalRel of L by ORDERS_2:def 5;

      end;

      then the InternalRel of K c= the InternalRel of L by RELAT_1:def 3;

      then

      reconsider K as SubRelStr of L by A2, YELLOW_0:def 13;

      now

        let x,y be object;

        assume

         A4: [x, y] in (the InternalRel of L |_2 the carrier of K);

        then

         A5: [x, y] in the InternalRel of L by XBOOLE_0:def 4;

        then

        reconsider p = x, q = y as Element of L by ZFMISC_1: 87;

         [x, y] in [:the carrier of K, the carrier of K:] by A4, XBOOLE_0:def 4;

        then

        reconsider p9 = x, q9 = y as Element of K by ZFMISC_1: 87;

        p <= q by A5, ORDERS_2:def 5;

        then for a be set st a in p holds ex b be set st b in q & b c= a by Th12;

        then p9 <= q9 by Th12;

        hence [x, y] in the InternalRel of K by ORDERS_2:def 5;

      end;

      then

       A6: (the InternalRel of L |_2 the carrier of K) c= the InternalRel of K by RELAT_1:def 3;

      now

        let x,y be object;

        assume

         A7: [x, y] in the InternalRel of K;

        then

        reconsider p = x, q = y as Element of K by ZFMISC_1: 87;

        reconsider p9 = p, q9 = q as Element of L by A2;

        p <= q by A7, ORDERS_2:def 5;

        then for a be set st a in p holds ex b be set st b in q & b c= a by Th12;

        then p9 <= q9 by Th12;

        then [p9, q9] in the InternalRel of L by ORDERS_2:def 5;

        hence [x, y] in (the InternalRel of L |_2 the carrier of K) by A7, XBOOLE_0:def 4;

      end;

      then the InternalRel of K c= (the InternalRel of L |_2 the carrier of K) by RELAT_1:def 3;

      then the InternalRel of K = (the InternalRel of L |_2 the carrier of K) by A6;

      hence thesis by YELLOW_0:def 14;

    end;

    definition

      let n,k be Nat;

      :: HEYTING3:def2

      func PFArt (n,k) -> Element of ( PFuncs ( NAT , {k})) means

      : Def2: for x be object holds x in it iff (ex m be odd Element of NAT st m <= (2 * n) & [m, k] = x) or [(2 * n), k] = x;

      existence

      proof

        defpred P[ object] means (ex m be odd Element of NAT st m <= (2 * n) & [m, k] = $1) or [(2 * n), k] = $1;

        consider X be set such that

         A1: for x be object holds x in X iff x in [: NAT , {k}:] & P[x] from XBOOLE_0:sch 1;

        

         A2: X c= [: NAT , {k}:] by A1;

        then

        reconsider X9 = X as Function by GRFUNC_1: 1;

        ( dom X9) c= NAT & ( rng X9) c= {k} by A2, SYSREL: 3;

        then

        reconsider X as Element of ( PFuncs ( NAT , {k})) by PARTFUN1:def 3;

        take X;

        let x be object;

        thus x in X implies (ex m be odd Element of NAT st m <= (2 * n) & [m, k] = x) or [(2 * n), k] = x by A1;

        assume

         A3: (ex m be odd Element of NAT st m <= (2 * n) & [m, k] = x) or [(2 * n), k] = x;

        

         A4: (2 * n) in NAT by ORDINAL1:def 12;

        per cases by A3;

          suppose ex m be odd Element of NAT st m <= (2 * n) & [m, k] = x;

          then x in [: NAT , {k}:] by ZFMISC_1: 106;

          hence thesis by A1, A3;

        end;

          suppose

           A5: [(2 * n), k] = x;

          then x in [: NAT , {k}:] by ZFMISC_1: 106, A4;

          hence thesis by A1, A5;

        end;

      end;

      uniqueness

      proof

        defpred P[ object] means (ex m be odd Element of NAT st m <= (2 * n) & [m, k] = $1) or [(2 * n), k] = $1;

        

         A6: for X1,X2 be Element of ( PFuncs ( NAT , {k})) 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 LMOD_7:sch 1;

        let X1,X2 be Element of ( PFuncs ( NAT , {k}));

        assume (for x be object holds x in X1 iff P[x]) & for x be object holds x in X2 iff P[x];

        hence thesis by A6;

      end;

    end

    registration

      let n,k be Element of NAT ;

      cluster ( PFArt (n,k)) -> finite;

      coherence

      proof

        ( PFArt (n,k)) c= [:(( Seg (2 * n)) \/ { 0 }), {k}:]

        proof

          let t be object;

          assume

           A1: t in ( PFArt (n,k));

          per cases by A1, Def2;

            suppose ex m1 be odd Element of NAT st m1 <= (2 * n) & [m1, k] = t;

            then

            consider m1 be odd Element of NAT such that

             A2: m1 <= (2 * n) and

             A3: [m1, k] = t;

            1 <= m1 by ABIAN: 12;

            then m1 in ( Seg (2 * n)) by A2, FINSEQ_1: 1;

            then m1 in (( Seg (2 * n)) \/ { 0 }) by XBOOLE_0:def 3;

            hence thesis by A3, ZFMISC_1: 106;

          end;

            suppose

             A4: [(2 * n), k] = t;

            now

              per cases ;

                suppose

                 A5: n is non zero;

                

                 A6: n <= (2 * n) by XREAL_1: 151;

                1 <= n by A5, NAT_1: 14;

                then 1 <= (2 * n) by A6, XXREAL_0: 2;

                then (2 * n) in ( Seg (2 * n)) by FINSEQ_1: 1;

                then (2 * n) in (( Seg (2 * n)) \/ { 0 }) by XBOOLE_0:def 3;

                hence thesis by A4, ZFMISC_1: 106;

              end;

                suppose n is zero;

                then (2 * n) in { 0 } by TARSKI:def 1;

                then (2 * n) in (( Seg (2 * n)) \/ { 0 }) by XBOOLE_0:def 3;

                hence thesis by A4, ZFMISC_1: 106;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let n,k be Nat;

      :: HEYTING3:def3

      func PFCrt (n,k) -> Element of ( PFuncs ( NAT , {k})) means

      : Def3: for x be object holds x in it iff ex m be odd Element of NAT st m <= ((2 * n) + 1) & [m, k] = x;

      existence

      proof

        defpred P[ object] means ex m be odd Element of NAT st m <= ((2 * n) + 1) & [m, k] = $1;

        consider X be set such that

         A1: for x be object holds x in X iff x in [: NAT , {k}:] & P[x] from XBOOLE_0:sch 1;

        

         A2: X c= [: NAT , {k}:] by A1;

        then

        reconsider X9 = X as Function by GRFUNC_1: 1;

        ( dom X9) c= NAT & ( rng X9) c= {k} by A2, SYSREL: 3;

        then

        reconsider X as Element of ( PFuncs ( NAT , {k})) by PARTFUN1:def 3;

        take X;

        let x be object;

        thus x in X implies ex m be odd Element of NAT st m <= ((2 * n) + 1) & [m, k] = x by A1;

        given m be odd Element of NAT such that

         A3: m <= ((2 * n) + 1) and

         A4: [m, k] = x;

        x in [: NAT , {k}:] by A4, ZFMISC_1: 106;

        hence thesis by A1, A3, A4;

      end;

      uniqueness

      proof

        defpred P[ object] means ex m be odd Element of NAT st m <= ((2 * n) + 1) & [m, k] = $1;

        

         A5: for X1,X2 be Element of ( PFuncs ( NAT , {k})) 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 LMOD_7:sch 1;

        let X1,X2 be Element of ( PFuncs ( NAT , {k}));

        assume (for x be object holds x in X1 iff P[x]) & for x be object holds x in X2 iff P[x];

        hence thesis by A5;

      end;

    end

    registration

      let n,k be Element of NAT ;

      cluster ( PFCrt (n,k)) -> finite;

      coherence

      proof

        set x = ( PFCrt (n,k));

        x c= [:( Seg ((2 * n) + 1)), {k}:]

        proof

          let t be object;

          assume t in x;

          then

          consider m be odd Element of NAT such that

           A1: m <= ((2 * n) + 1) and

           A2: [m, k] = t by Def3;

          1 <= m by ABIAN: 12;

          then m in ( Seg ((2 * n) + 1)) by A1, FINSEQ_1: 1;

          hence thesis by A2, ZFMISC_1: 106;

        end;

        hence thesis;

      end;

    end

    theorem :: HEYTING3:14

    for n,k be Element of NAT holds [((2 * n) + 1), k] in ( PFCrt (n,k)) by Def3;

    theorem :: HEYTING3:15

    

     Th15: for n,k be Element of NAT holds ( PFCrt (n,k)) misses { [((2 * n) + 3), k]}

    proof

      let n,k be Element of NAT ;

      assume (( PFCrt (n,k)) /\ { [((2 * n) + 3), k]}) <> {} ;

      then

      consider x be object such that

       A1: x in (( PFCrt (n,k)) /\ { [((2 * n) + 3), k]}) by XBOOLE_0:def 1;

      x in ( PFCrt (n,k)) by A1, XBOOLE_0:def 4;

      then

      consider m be odd Element of NAT such that

       A2: m <= ((2 * n) + 1) and

       A3: [m, k] = x by Def3;

      x in { [((2 * n) + 3), k]} by A1, XBOOLE_0:def 4;

      then x = [((2 * n) + 3), k] by TARSKI:def 1;

      then m = ((2 * n) + 3) by A3, XTUPLE_0: 1;

      hence thesis by A2, XREAL_1: 6;

    end;

    

     Lm4: for n be Element of NAT holds ((2 * n) + 1) <= ((2 * (n + 1)) + 1)

    proof

      let n be Element of NAT ;

      ((2 * (n + 1)) + 1) = (((2 * n) + 1) + 2);

      hence thesis by NAT_1: 11;

    end;

    theorem :: HEYTING3:16

    

     Th16: for n,k be Element of NAT holds ( PFCrt ((n + 1),k)) = (( PFCrt (n,k)) \/ { [((2 * n) + 3), k]})

    proof

      let n,k be Element of NAT ;

      

       A1: ((2 * (n + 1)) + 1) = ((2 * n) + 3);

      thus ( PFCrt ((n + 1),k)) c= (( PFCrt (n,k)) \/ { [((2 * n) + 3), k]})

      proof

        let x be object;

        assume x in ( PFCrt ((n + 1),k));

        then

        consider m be odd Element of NAT such that

         A2: m <= ((2 * (n + 1)) + 1) and

         A3: [m, k] = x by Def3;

        per cases by A2, NAT_1: 9;

          suppose m <= (2 * (n + 1));

          then m <= ((2 * n) + 1) or m = (((2 * n) + 1) + 1) by NAT_1: 8;

          then x in ( PFCrt (n,k)) by A3, Def3;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose m = ((2 * (n + 1)) + 1);

          then x in { [((2 * n) + 3), k]} by A3, TARSKI:def 1;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      let x be object;

      assume

       A4: x in (( PFCrt (n,k)) \/ { [((2 * n) + 3), k]});

      per cases by A4, XBOOLE_0:def 3;

        suppose x in ( PFCrt (n,k));

        then

        consider m be odd Element of NAT such that

         A5: m <= ((2 * n) + 1) and

         A6: [m, k] = x by Def3;

        ((2 * n) + 1) <= ((2 * (n + 1)) + 1) by Lm4;

        then m <= ((2 * (n + 1)) + 1) by A5, XXREAL_0: 2;

        hence thesis by A6, Def3;

      end;

        suppose x in { [((2 * n) + 3), k]};

        then x = [((2 * n) + 3), k] by TARSKI:def 1;

        hence thesis by A1, Def3;

      end;

    end;

    

     Lm5: for n,n9 be Element of NAT holds not ( PFCrt ((n + 1),n9)) c= ( PFCrt (n,n9))

    proof

      let n,n9 be Element of NAT ;

      set k = [((2 * n) + 3), n9];

      ( PFCrt ((n + 1),n9)) = (( PFCrt (n,n9)) \/ { [((2 * n) + 3), n9]}) by Th16;

      then {k} c= ( PFCrt ((n + 1),n9)) by XBOOLE_1: 7;

      then

       A1: k in ( PFCrt ((n + 1),n9)) by ZFMISC_1: 31;

      ( PFCrt (n,n9)) misses { [((2 * n) + 3), n9]} by Th15;

      then (( PFCrt (n,n9)) /\ { [((2 * n) + 3), n9]}) = {} ;

      hence thesis by A1, ZFMISC_1: 46;

    end;

    theorem :: HEYTING3:17

    

     Th17: for n,k be Element of NAT holds ( PFCrt (n,k)) c< ( PFCrt ((n + 1),k))

    proof

      let n,k be Element of NAT ;

      thus ( PFCrt (n,k)) c= ( PFCrt ((n + 1),k))

      proof

        let x be object;

        assume x in ( PFCrt (n,k));

        then

        consider m be odd Element of NAT such that

         A1: m <= ((2 * n) + 1) and

         A2: [m, k] = x by Def3;

        ((2 * n) + 1) <= ((2 * (n + 1)) + 1) by Lm4;

        then m <= ((2 * (n + 1)) + 1) by A1, XXREAL_0: 2;

        hence thesis by A2, Def3;

      end;

      thus thesis by Lm5;

    end;

    registration

      let n,k be Element of NAT ;

      cluster ( PFArt (n,k)) -> non empty;

      coherence

      proof

         [(2 * n), k] in ( PFArt (n,k)) by Def2;

        hence thesis;

      end;

    end

    theorem :: HEYTING3:18

    

     Th18: for n,m,k be Element of NAT holds not ( PFArt (n,m)) c= ( PFCrt (k,m))

    proof

      let n,m,k be Element of NAT ;

      set x = [(2 * n), m];

      

       A1: not x in ( PFCrt (k,m))

      proof

        assume x in ( PFCrt (k,m));

        then ex m9 be odd Element of NAT st m9 <= ((2 * k) + 1) & [m9, m] = x by Def3;

        hence thesis by XTUPLE_0: 1;

      end;

      x in ( PFArt (n,m)) by Def2;

      hence thesis by A1;

    end;

    

     Lm6: for n,k be Element of NAT holds ( PFCrt (n,k)) c= ( PFCrt ((n + 1),k))

    proof

      let n,k be Element of NAT ;

      ( PFCrt (n,k)) c< ( PFCrt ((n + 1),k)) by Th17;

      hence thesis;

    end;

    theorem :: HEYTING3:19

    for n,m,k be Element of NAT st n <= k holds ( PFCrt (n,m)) c= ( PFCrt (k,m))

    proof

      let n,m,k be Element of NAT ;

      assume n <= k;

      then (2 * n) <= (2 * k) by NAT_1: 4;

      then

       A1: ((2 * n) + 1) <= ((2 * k) + 1) by XREAL_1: 6;

      let x be object;

      assume x in ( PFCrt (n,m));

      then

      consider m9 be odd Element of NAT such that

       A2: m9 <= ((2 * n) + 1) and

       A3: [m9, m] = x by Def3;

      m9 <= ((2 * k) + 1) by A1, A2, XXREAL_0: 2;

      hence thesis by A3, Def3;

    end;

    

     Lm7: for n,m,k be Element of NAT st n < k holds ( PFCrt (n,m)) c= ( PFArt (k,m))

    proof

      let n,m,k be Element of NAT ;

      assume n < k;

      then (2 * n) < (2 * k) by XREAL_1: 68;

      then

       A1: ((2 * n) + 1) <= (2 * k) by NAT_1: 13;

      let x be object;

      assume x in ( PFCrt (n,m));

      then

      consider p be odd Element of NAT such that

       A2: p <= ((2 * n) + 1) and

       A3: [p, m] = x by Def3;

      p <= (2 * k) by A1, A2, XXREAL_0: 2;

      hence thesis by A3, Def2;

    end;

    theorem :: HEYTING3:20

    for n be Element of NAT holds ( PFArt (1,n)) = { [1, n], [2, n]}

    proof

      let n be Element of NAT ;

      thus ( PFArt (1,n)) c= { [1, n], [2, n]}

      proof

        let x be object;

        assume

         A1: x in ( PFArt (1,n));

        per cases by A1, Def2;

          suppose ex m be odd Element of NAT st m <= (2 * 1) & [m, n] = x;

          then

          consider m be odd Element of NAT such that

           A2: m <= (2 * 1) & [m, n] = x;

          m = 0 or ... or m = 2 by A2;

          then x = [1, n] by A2;

          hence thesis by TARSKI:def 2;

        end;

          suppose [(2 * 1), n] = x;

          hence thesis by TARSKI:def 2;

        end;

      end;

      let x be object;

      assume

       A3: x in { [1, n], [2, n]};

      per cases by A3, TARSKI:def 2;

        suppose

         A4: x = [1, n];

        1 <= (2 * 1);

        hence thesis by A4, Def2, Lm2, Lm3;

      end;

        suppose x = [2, n];

        then x = [(2 * 1), n];

        hence thesis by Def2;

      end;

    end;

    definition

      let n,k be Nat;

      :: HEYTING3:def4

      func PFBrt (n,k) -> Element of ( Fin ( PFuncs ( NAT , {k}))) means

      : Def4: for x be object holds x in it iff (ex m be non zero Element of NAT st m <= n & x = ( PFArt (m,k))) or x = ( PFCrt (n,k));

      existence

      proof

        defpred P[ object] means (ex m be non zero Element of NAT st m <= n & $1 = ( PFArt (m,k))) or $1 = ( PFCrt (n,k));

        consider X be set such that

         A1: for x be object holds x in X iff x in ( PFuncs ( NAT , {k})) & P[x] from XBOOLE_0:sch 1;

        

         A2: X c= ( bool [:( Seg ((2 * n) + 1)), {k}:])

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume

           A3: x in X;

          per cases by A1, A3;

            suppose

             A4: ex m be non zero Element of NAT st m <= n & x = ( PFArt (m,k));

            

             A5: (2 * n) <= ((2 * n) + 1) by NAT_1: 11;

            consider m be non zero Element of NAT such that

             A6: m <= n and

             A7: x = ( PFArt (m,k)) by A4;

            (2 * m) <= (2 * n) by A6, NAT_1: 4;

            then

             A8: (2 * m) <= ((2 * n) + 1) by A5, XXREAL_0: 2;

            xx c= [:( Seg ((2 * n) + 1)), {k}:]

            proof

              let t be object;

              assume

               A9: t in xx;

              per cases by A7, A9, Def2;

                suppose ex m1 be odd Element of NAT st m1 <= (2 * m) & [m1, k] = t;

                then

                consider m1 be odd Element of NAT such that

                 A10: m1 <= (2 * m) and

                 A11: [m1, k] = t;

                

                 A12: 1 <= m1 by ABIAN: 12;

                m1 <= ((2 * n) + 1) by A8, A10, XXREAL_0: 2;

                then m1 in ( Seg ((2 * n) + 1)) by A12, FINSEQ_1: 1;

                hence thesis by A11, ZFMISC_1: 106;

              end;

                suppose

                 A13: [(2 * m), k] = t;

                1 <= (2 * m) by NAT_1: 14;

                then (2 * m) in ( Seg ((2 * n) + 1)) by A8, FINSEQ_1: 1;

                hence thesis by A13, ZFMISC_1: 106;

              end;

            end;

            hence thesis;

          end;

            suppose

             A14: x = ( PFCrt (n,k));

            xx c= [:( Seg ((2 * n) + 1)), {k}:]

            proof

              let t be object;

              assume t in xx;

              then

              consider m be odd Element of NAT such that

               A15: m <= ((2 * n) + 1) and

               A16: [m, k] = t by A14, Def3;

              1 <= m by ABIAN: 12;

              then m in ( Seg ((2 * n) + 1)) by A15, FINSEQ_1: 1;

              hence thesis by A16, ZFMISC_1: 106;

            end;

            hence thesis;

          end;

        end;

        X c= ( PFuncs ( NAT , {k})) by A1;

        then

        reconsider X as Element of ( Fin ( PFuncs ( NAT , {k}))) by A2, FINSUB_1:def 5;

        take X;

        let x be object;

        thus x in X implies (ex m be non zero Element of NAT st m <= n & x = ( PFArt (m,k))) or x = ( PFCrt (n,k)) by A1;

        assume (ex m be non zero Element of NAT st m <= n & x = ( PFArt (m,k))) or x = ( PFCrt (n,k));

        hence thesis by A1;

      end;

      uniqueness

      proof

        defpred P[ object] means (ex m be non zero Element of NAT st m <= n & $1 = ( PFArt (m,k))) or $1 = ( PFCrt (n,k));

        

         A17: for X1,X2 be Element of ( Fin ( PFuncs ( NAT , {k}))) 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 LMOD_7:sch 1;

        let X1,X2 be Element of ( Fin ( PFuncs ( NAT , {k})));

        assume (for x be object holds x in X1 iff P[x]) & for x be object holds x in X2 iff P[x];

        hence thesis by A17;

      end;

    end

    theorem :: HEYTING3:21

    for n,k be Element of NAT , x be set st x in ( PFBrt ((n + 1),k)) holds ex y be set st y in ( PFBrt (n,k)) & y c= x

    proof

      let n,k be Element of NAT , x be set;

      assume

       A1: x in ( PFBrt ((n + 1),k));

      per cases by A1, Def4;

        suppose ex m be non zero Element of NAT st m <= (n + 1) & x = ( PFArt (m,k));

        then

        consider m be non zero Element of NAT such that

         A2: m <= (n + 1) and

         A3: x = ( PFArt (m,k));

        thus ex y be set st y in ( PFBrt (n,k)) & y c= x

        proof

          per cases by A2, NAT_1: 8;

            suppose

             A4: m <= n;

            take y = x;

            thus y in ( PFBrt (n,k)) by A3, A4, Def4;

            thus thesis;

          end;

            suppose

             A5: m = (n + 1);

            take ( PFCrt (n,k));

            n < (n + 1) by NAT_1: 13;

            hence thesis by A3, A5, Def4, Lm7;

          end;

        end;

      end;

        suppose

         A6: x = ( PFCrt ((n + 1),k));

        take y = ( PFCrt (n,k));

        thus y in ( PFBrt (n,k)) by Def4;

        thus thesis by A6, Lm6;

      end;

    end;

    theorem :: HEYTING3:22

    for n,k be Element of NAT holds not ( PFCrt (n,k)) in ( PFBrt ((n + 1),k))

    proof

      let n,k be Element of NAT ;

      assume ( PFCrt (n,k)) in ( PFBrt ((n + 1),k));

      then (ex m be non zero Element of NAT st m <= (n + 1) & ( PFCrt (n,k)) = ( PFArt (m,k))) or ( PFCrt (n,k)) = ( PFCrt ((n + 1),k)) by Def4;

      hence thesis by Th17, Th18;

    end;

    

     Lm8: for n,k be Element of NAT , x be set st x in ( PFBrt (n,k)) holds x is finite

    proof

      let n,k be Element of NAT , x be set;

      assume x in ( PFBrt (n,k));

      then

       A1: (ex m be non zero Element of NAT st m <= n & x = ( PFArt (m,k))) or x = ( PFCrt (n,k)) by Def4;

      per cases by A1;

        suppose ex m be Element of NAT st m <= n & x = ( PFArt (m,k));

        hence thesis;

      end;

        suppose x = ( PFCrt (n,k));

        hence thesis;

      end;

    end;

    theorem :: HEYTING3:23

    

     Th23: for n,m,k be Element of NAT st ( PFArt (n,m)) c= ( PFArt (k,m)) holds n = k

    proof

      let n,m,k be Element of NAT ;

      assume

       A1: ( PFArt (n,m)) c= ( PFArt (k,m));

      assume n <> k;

      then (2 * n) <> (2 * k);

      then

       A2: [(2 * n), m] <> [(2 * k), m] by XTUPLE_0: 1;

       [(2 * n), m] in ( PFArt (n,m)) by Def2;

      then ex m9 be odd Element of NAT st m9 <= (2 * k) & [m9, m] = [(2 * n), m] by A1, A2, Def2;

      hence thesis by XTUPLE_0: 1;

    end;

    theorem :: HEYTING3:24

    

     Th24: for n,m,k be Element of NAT holds ( PFCrt (n,m)) c= ( PFArt (k,m)) iff n < k

    proof

      let n,m,k be Element of NAT ;

      thus ( PFCrt (n,m)) c= ( PFArt (k,m)) implies n < k

      proof

        assume

         A1: ( PFCrt (n,m)) c= ( PFArt (k,m));

        assume

         A2: k <= n;

        

         A3: not [((2 * n) + 1), m] in ( PFArt (k,m))

        proof

          assume

           A4: [((2 * n) + 1), m] in ( PFArt (k,m));

          per cases by A4, Def2;

            suppose

             A5: ex m9 be odd Element of NAT st m9 <= (2 * k) & [m9, m] = [((2 * n) + 1), m];

            

             A6: (2 * k) <= (2 * n) by A2, NAT_1: 4;

            ((2 * n) + 1) <= (2 * k) by A5, XTUPLE_0: 1;

            hence thesis by A6, NAT_1: 13;

          end;

            suppose [(2 * k), m] = [((2 * n) + 1), m];

            hence thesis by XTUPLE_0: 1;

          end;

        end;

         [((2 * n) + 1), m] in ( PFCrt (n,m)) by Def3;

        hence thesis by A1, A3;

      end;

      thus thesis by Lm7;

    end;

    begin

    theorem :: HEYTING3:25

    

     Th25: for n,k be Element of NAT holds ( PFBrt (n,k)) is Element of ( SubstPoset ( NAT , {k}))

    proof

      let n,k be Element of NAT ;

      

       A1: for s,t be Element of ( PFuncs ( NAT , {k})) holds (s in ( PFBrt (n,k)) & t in ( PFBrt (n,k)) & s c= t implies s = t)

      proof

        let s,t be Element of ( PFuncs ( NAT , {k}));

        assume that

         A2: s in ( PFBrt (n,k)) and

         A3: t in ( PFBrt (n,k)) and

         A4: s c= t;

        

         A5: (ex m be non zero Element of NAT st m <= n & s = ( PFArt (m,k))) or s = ( PFCrt (n,k)) by A2, Def4;

        

         A6: (ex m be non zero Element of NAT st m <= n & t = ( PFArt (m,k))) or t = ( PFCrt (n,k)) by A3, Def4;

        per cases by A5, A6;

          suppose (ex m be Element of NAT st m <= n & s = ( PFArt (m,k))) & ex m be Element of NAT st m <= n & t = ( PFArt (m,k));

          hence thesis by A4, Th23;

        end;

          suppose (ex m be Element of NAT st m <= n & s = ( PFArt (m,k))) & t = ( PFCrt (n,k));

          hence thesis by A4, Th18;

        end;

          suppose s = ( PFCrt (n,k)) & ex m be Element of NAT st m <= n & t = ( PFArt (m,k));

          hence thesis by A4, Th24;

        end;

          suppose s = ( PFCrt (n,k)) & t = ( PFCrt (n,k));

          hence thesis;

        end;

      end;

      for u be set st u in ( PFBrt (n,k)) holds u is finite by Lm8;

      then ( SubstitutionSet ( NAT , {k})) = the carrier of ( SubstPoset ( NAT , {k})) & ( PFBrt (n,k)) in { A where A be Element of ( Fin ( PFuncs ( NAT , {k}))) : (for u be set st u in A holds u is finite) & for s,t be Element of ( PFuncs ( NAT , {k})) holds (s in A & t in A & s c= t implies s = t) } by A1, SUBSTLAT:def 4;

      hence thesis by SUBSTLAT:def 1;

    end;

    definition

      let k be Element of NAT ;

      :: HEYTING3:def5

      func PFDrt k -> Subset of ( SubstPoset ( NAT , {k})) means

      : Def5: for x be object holds x in it iff ex n be non zero Element of NAT st x = ( PFBrt (n,k));

      existence

      proof

        defpred P[ object] means ex n be non zero Element of NAT st $1 = ( PFBrt (n,k));

        consider X be set such that

         A1: for x be object holds x in X iff x in the carrier of ( SubstPoset ( NAT , {k})) & P[x] from XBOOLE_0:sch 1;

        X c= the carrier of ( SubstPoset ( NAT , {k})) by A1;

        then

        reconsider X9 = X as Subset of ( SubstPoset ( NAT , {k}));

        take X9;

        let x be object;

        thus x in X9 implies ex n be non zero Element of NAT st x = ( PFBrt (n,k)) by A1;

        given n be non zero Element of NAT such that

         A2: x = ( PFBrt (n,k));

        x is Element of ( SubstPoset ( NAT , {k})) by A2, Th25;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        defpred P[ object] means ex n be non zero Element of NAT st $1 = ( PFBrt (n,k));

        

         A3: for A1,A2 be Subset of ( SubstPoset ( NAT , {k})) st (for x be object holds x in A1 iff P[x]) & (for x be object holds x in A2 iff P[x]) holds A1 = A2 from SSubsetUniq;

        let A1,A2 be Subset of ( SubstPoset ( NAT , {k}));

        assume (for x be object holds x in A1 iff P[x]) & for x be object holds x in A2 iff P[x];

        hence thesis by A3;

      end;

    end

    theorem :: HEYTING3:26

    for k be Element of NAT holds ( PFBrt (1,k)) = {( PFArt (1,k)), ( PFCrt (1,k))}

    proof

      let k be Element of NAT ;

      thus ( PFBrt (1,k)) c= {( PFArt (1,k)), ( PFCrt (1,k))}

      proof

        let x be object;

        assume

         A1: x in ( PFBrt (1,k));

        per cases by A1, Def4;

          suppose ex m be non zero Element of NAT st m <= 1 & x = ( PFArt (m,k));

          then

          consider m be non zero Element of NAT such that

           A2: m <= 1 and

           A3: x = ( PFArt (m,k));

          m >= 1 by NAT_1: 14;

          then m = 1 by A2, XXREAL_0: 1;

          hence thesis by A3, TARSKI:def 2;

        end;

          suppose x = ( PFCrt (1,k));

          hence thesis by TARSKI:def 2;

        end;

      end;

      let x be object;

      assume

       A4: x in {( PFArt (1,k)), ( PFCrt (1,k))};

      per cases by A4, TARSKI:def 2;

        suppose x = ( PFArt (1,k));

        hence thesis by Def4;

      end;

        suppose x = ( PFCrt (1,k));

        hence thesis by Def4;

      end;

    end;

    theorem :: HEYTING3:27

    

     Th27: for k be Element of NAT holds ( PFBrt (1,k)) <> { {} }

    proof

      let k be Element of NAT ;

      ( PFArt (1,k)) in ( PFBrt (1,k)) by Def4;

      hence thesis by TARSKI:def 1;

    end;

    registration

      let k be Element of NAT ;

      cluster ( PFBrt (1,k)) -> non empty;

      coherence

      proof

        ( PFArt (1,k)) in ( PFBrt (1,k)) by Def4;

        hence thesis;

      end;

    end

    theorem :: HEYTING3:28

    

     Th28: for n,k be Element of NAT holds {( PFArt (n,k))} is Element of ( SubstPoset ( NAT , {k}))

    proof

      let n,k be Element of NAT ;

      ( SubstitutionSet ( NAT , {k})) = the carrier of ( SubstPoset ( NAT , {k})) by SUBSTLAT:def 4;

      hence thesis by HEYTING2: 2;

    end;

    theorem :: HEYTING3:29

    

     Th29: for k be Element of NAT , V,X be set, a be Element of ( SubstPoset (V, {k})) st X in a holds X is finite Subset of [:V, {k}:]

    proof

      let k be Element of NAT ;

      let V,X be set;

      let a be Element of ( SubstPoset (V, {k}));

      assume

       A1: X in a;

      

       A2: ( PFuncs (V, {k})) c= ( bool [:V, {k}:]) by PRE_POLY: 16;

      

       A3: ( SubstitutionSet (V, {k})) = the carrier of ( SubstPoset (V, {k})) by SUBSTLAT:def 4;

      then a in ( SubstitutionSet (V, {k}));

      then a c= ( PFuncs (V, {k})) by FINSUB_1:def 5;

      then X in ( PFuncs (V, {k})) by A1;

      hence thesis by A3, A1, A2, HEYTING2: 1;

    end;

    theorem :: HEYTING3:30

    

     Th30: for m be Element of NAT , a be Element of ( SubstPoset ( NAT , {m})) st ( PFDrt m) is_>=_than a holds for X be non empty set st X in a holds not (for n be Element of NAT st [n, m] in X holds n is odd)

    proof

      let m be Element of NAT ;

      let a be Element of ( SubstPoset ( NAT , {m}));

      assume

       A1: ( PFDrt m) is_>=_than a;

      let X be non empty set;

      assume

       A2: X in a;

      then

      reconsider X9 = X as finite non empty Subset of [: NAT , {m}:] by Th29;

      assume

       A3: for n be Element of NAT st [n, m] in X holds n is odd;

       A4:

      now

        let k be non zero Element of NAT ;

        reconsider Pk = ( PFBrt (k,m)) as Element of ( SubstPoset ( NAT , {m})) by Th25;

        

         A5: [((2 * k) + 1), m] in ( PFCrt (k,m)) by Def3;

        Pk in ( PFDrt m) by Def5;

        then a <= Pk by A1;

        then

        consider y be set such that

         A6: y in Pk and

         A7: y c= X by A2, Th12;

        

         A8: not ex m9 be Element of NAT st m9 <= k & y = ( PFArt (m9,m))

        proof

          given m9 be Element of NAT such that m9 <= k and

           A9: y = ( PFArt (m9,m));

           [(2 * m9), m] in ( PFArt (m9,m)) by Def2;

          hence thesis by A3, A7, A9;

        end;

        (ex m9 be non zero Element of NAT st m9 <= k & y = ( PFArt (m9,m))) or y = ( PFCrt (k,m)) by A6, Def4;

        hence [((2 * k) + 1), m] in X by A7, A8, A5;

      end;

      ex l be non zero Element of NAT st not [((2 * l) + 1), m] in X9 by Th4;

      hence thesis by A4;

    end;

    theorem :: HEYTING3:31

    

     Th31: for k be Element of NAT , a,b be Element of ( SubstPoset ( NAT , {k})), X be Subset of ( SubstPoset ( NAT , {k})) st a is_<=_than X & b is_<=_than X holds (a "\/" b) is_<=_than X

    proof

      let k be Element of NAT ;

      let a,b be Element of ( SubstPoset ( NAT , {k})), X be Subset of ( SubstPoset ( NAT , {k}));

      assume

       A1: a is_<=_than X & b is_<=_than X;

      let c be Element of ( SubstPoset ( NAT , {k}));

      assume c in X;

      then a <= c & b <= c by A1;

      hence thesis by YELLOW_5: 9;

    end;

    registration

      let k be Element of NAT ;

      cluster non empty for Element of ( SubstPoset ( NAT , {k}));

      existence

      proof

        ( SubstitutionSet ( NAT , {k})) = the carrier of ( SubstPoset ( NAT , {k})) by SUBSTLAT:def 4;

        then

        reconsider E = { {} } as Element of ( SubstPoset ( NAT , {k})) by SUBSTLAT: 2;

        take E;

        thus thesis;

      end;

    end

    

     Lm9: for a be non empty set st a <> { {} } & {} in a holds ex b be set st b in a & b <> {}

    proof

      let a be non empty set;

      assume that

       A1: a <> { {} } and

       A2: {} in a;

      assume

       A3: for b be set st b in a holds b = {} ;

      a = { {} }

      proof

        thus a c= { {} }

        proof

          let x be object;

          assume x in a;

          then x = {} by A3;

          hence thesis by TARSKI:def 1;

        end;

        let x be object;

        assume x in { {} };

        hence thesis by A2, TARSKI:def 1;

      end;

      hence thesis by A1;

    end;

    theorem :: HEYTING3:32

    

     Th32: for n be Element of NAT , a be Element of ( SubstPoset ( NAT , {n})) st {} in a holds a = { {} }

    proof

      let n be Element of NAT ;

      let a be Element of ( SubstPoset ( NAT , {n}));

      assume

       A1: {} in a;

      ( SubstitutionSet ( NAT , {n})) = the carrier of ( SubstPoset ( NAT , {n})) by SUBSTLAT:def 4;

      then

       A2: a in ( SubstitutionSet ( NAT , {n}));

      assume a <> { {} };

      then ex k be set st k in a & k <> {} by A1, Lm9;

      hence thesis by A2, A1, SUBSTLAT: 5, XBOOLE_1: 2;

    end;

    theorem :: HEYTING3:33

    

     Th33: for k be Element of NAT , a be non empty Element of ( SubstPoset ( NAT , {k})) st a <> { {} } holds ex f be finite Function st f in a & f <> {}

    proof

      let k be Element of NAT ;

      let a be non empty Element of ( SubstPoset ( NAT , {k}));

      assume

       A1: a <> { {} };

      consider f be object such that

       A2: f in a by XBOOLE_0:def 1;

      ( SubstitutionSet ( NAT , {k})) = the carrier of ( SubstPoset ( NAT , {k})) by SUBSTLAT:def 4;

      then

      reconsider f as finite Function by A2, HEYTING2: 1;

      take f;

      thus f in a by A2;

      assume f = {} ;

      hence thesis by A1, A2, Th32;

    end;

    theorem :: HEYTING3:34

    

     Th34: for k be Element of NAT , a be non empty Element of ( SubstPoset ( NAT , {k})), a9 be Element of ( Fin ( PFuncs ( NAT , {k}))) st a <> { {} } & a = a9 holds ( Involved a9) is finite non empty Subset of NAT

    proof

      let k be Element of NAT ;

      let a be non empty Element of ( SubstPoset ( NAT , {k}));

      let a9 be Element of ( Fin ( PFuncs ( NAT , {k})));

      assume that

       A1: a <> { {} } and

       A2: a = a9;

      consider f be finite Function such that

       A3: f in a and

       A4: f <> {} by A1, Th33;

      ex k1 be object st k1 in ( dom f) by A4, XBOOLE_0:def 1;

      hence thesis by A2, A3, HEYTING2: 6, HEYTING2:def 1;

    end;

    theorem :: HEYTING3:35

    

     Th35: for k be Element of NAT , a be Element of ( SubstPoset ( NAT , {k})), a9 be Element of ( Fin ( PFuncs ( NAT , {k}))), B be finite non empty Subset of NAT st B = ( Involved a9) & a9 = a holds for X be set st X in a holds for l be Element of NAT st l > (( max B) + 1) holds not [l, k] in X

    proof

      let k be Element of NAT , a be Element of ( SubstPoset ( NAT , {k})), a9 be Element of ( Fin ( PFuncs ( NAT , {k}))), B be finite non empty Subset of NAT ;

      assume that

       A1: B = ( Involved a9) and

       A2: a9 = a;

      let X be set;

      assume

       A3: X in a;

      ( SubstitutionSet ( NAT , {k})) = the carrier of ( SubstPoset ( NAT , {k})) by SUBSTLAT:def 4;

      then

      reconsider X9 = X as finite Function by A3, HEYTING2: 1;

      let l be Element of NAT ;

      assume

       A4: l > (( max B) + 1);

      assume [l, k] in X;

      then l in ( dom X9) by XTUPLE_0:def 12;

      then l in ( Involved a9) by A2, A3, HEYTING2:def 1;

      then (( max B) + 1) >= ( max B) & ( max B) >= l by A1, NAT_1: 11, XXREAL_2:def 8;

      hence thesis by A4, XXREAL_0: 2;

    end;

    theorem :: HEYTING3:36

    

     Th36: for k be Element of NAT holds ( Top ( SubstPoset ( NAT , {k}))) = { {} }

    proof

      let k be Element of NAT ;

      ( SubstitutionSet ( NAT , {k})) = the carrier of ( SubstPoset ( NAT , {k})) by SUBSTLAT:def 4;

      then

      reconsider a = { {} } as Element of ( SubstPoset ( NAT , {k})) by SUBSTLAT: 2;

      

       A1: for b be Element of ( SubstPoset ( NAT , {k})) st b is_<=_than {} holds a >= b

      proof

        let b be Element of ( SubstPoset ( NAT , {k}));

        assume b is_<=_than {} ;

        now

          let x be set;

          assume x in b;

          take y = {} ;

          thus y in a & y c= x by TARSKI:def 1;

        end;

        hence thesis by Th12;

      end;

      a is_<=_than {} ;

      then a = ( "/\" ( {} ,( SubstPoset ( NAT , {k})))) by A1, YELLOW_0: 31;

      hence thesis by YELLOW_0:def 12;

    end;

    theorem :: HEYTING3:37

    

     Th37: for k be Element of NAT holds ( Bottom ( SubstPoset ( NAT , {k}))) = {}

    proof

      let k be Element of NAT ;

      ( SubstitutionSet ( NAT , {k})) = the carrier of ( SubstPoset ( NAT , {k})) by SUBSTLAT:def 4;

      then

      reconsider a = {} as Element of ( SubstPoset ( NAT , {k})) by SUBSTLAT: 1;

      

       A1: for b be Element of ( SubstPoset ( NAT , {k})) st b is_>=_than {} holds a <= b

      proof

        let b be Element of ( SubstPoset ( NAT , {k}));

        assume b is_>=_than {} ;

        for x be set st x in a holds ex y be set st y in b & y c= x;

        hence thesis by Th12;

      end;

      a is_>=_than {} ;

      then a = ( "\/" ( {} ,( SubstPoset ( NAT , {k})))) by A1, YELLOW_0: 30;

      hence thesis by YELLOW_0:def 11;

    end;

    theorem :: HEYTING3:38

    

     Th38: for k be Element of NAT , a,b be Element of ( SubstPoset ( NAT , {k})) st a <= b & a = { {} } holds b = { {} }

    proof

      let k be Element of NAT , a,b be Element of ( SubstPoset ( NAT , {k}));

      assume

       A1: a <= b & a = { {} };

      ( Top ( SubstPoset ( NAT , {k}))) = { {} } by Th36;

      hence thesis by A1, WAYBEL15: 3;

    end;

    theorem :: HEYTING3:39

    

     Th39: for k be Element of NAT , a,b be Element of ( SubstPoset ( NAT , {k})) st a <= b & b = {} holds a = {}

    proof

      let k be Element of NAT , a,b be Element of ( SubstPoset ( NAT , {k}));

      assume

       A1: a <= b & b = {} ;

      ( Bottom ( SubstPoset ( NAT , {k}))) = {} by Th37;

      hence thesis by A1, YELLOW_5: 19;

    end;

    theorem :: HEYTING3:40

    

     Th40: for m be Element of NAT , a be Element of ( SubstPoset ( NAT , {m})) st ( PFDrt m) is_>=_than a holds a <> { {} }

    proof

      let m be Element of NAT ;

      reconsider P1 = ( PFBrt (1,m)) as Element of ( SubstPoset ( NAT , {m})) by Th25;

      let a be Element of ( SubstPoset ( NAT , {m}));

      assume

       A1: ( PFDrt m) is_>=_than a;

      ( PFBrt (1,m)) in ( PFDrt m) by Def5;

      then

       A2: P1 >= a by A1;

      assume

       A3: a = { {} };

      ( Top ( SubstPoset ( NAT , {m}))) = { {} } by Th36;

      hence thesis by A3, A2, Th27, WAYBEL15: 3;

    end;

    

     Lm10: for m be Element of NAT holds not ( SubstPoset ( NAT , {m})) is complete

    proof

      let m be Element of NAT ;

      reconsider Cos = {( PFArt (1,m))} as Element of ( SubstPoset ( NAT , {m})) by Th28;

      assume ( SubstPoset ( NAT , {m})) is complete;

      then

      consider a be Element of ( SubstPoset ( NAT , {m})) such that

       A1: ( PFDrt m) is_>=_than a and

       A2: for b be Element of ( SubstPoset ( NAT , {m})) st ( PFDrt m) is_>=_than b holds a >= b by LATTICE5:def 2;

      ( SubstitutionSet ( NAT , {m})) = the carrier of ( SubstPoset ( NAT , {m})) by SUBSTLAT:def 4;

      then a in ( SubstitutionSet ( NAT , {m}));

      then

      reconsider a9 = a as Element of ( Fin ( PFuncs ( NAT , {m})));

      set Mi = ( Involved a9);

      ( PFDrt m) is_>=_than Cos

      proof

        let u be Element of ( SubstPoset ( NAT , {m}));

        assume u in ( PFDrt m);

        then

        consider n1 be non zero Element of NAT such that

         A3: u = ( PFBrt (n1,m)) by Def5;

        now

          let d be set;

          assume d in Cos;

          then

           A4: d = ( PFArt (1,m)) by TARSKI:def 1;

          1 <= n1 by NAT_1: 14;

          then d in ( PFBrt (n1,m)) by A4, Def4;

          hence ex e be set st e in u & e c= d by A3;

        end;

        hence thesis by Th12;

      end;

      then a <> {} by A2, Th39;

      then

      reconsider Mi as finite non empty Subset of NAT by A1, Th34, Th40;

      reconsider mX = (( max Mi) + 1) as non zero Element of NAT ;

      reconsider Sum = {( PFArt (mX,m))} as Element of ( SubstPoset ( NAT , {m})) by Th28;

      set b = (a "\/" Sum);

      Sum is_<=_than ( PFDrt m)

      proof

        let t be Element of ( SubstPoset ( NAT , {m}));

        assume t in ( PFDrt m);

        then

        consider n be non zero Element of NAT such that

         A5: t = ( PFBrt (n,m)) by Def5;

        for x be set st x in Sum holds ex y be set st y in t & y c= x

        proof

          let x be set;

          assume

           A6: x in Sum;

          then

           A7: x = ( PFArt (mX,m)) by TARSKI:def 1;

          per cases ;

            suppose

             A8: n < mX;

            take y = ( PFCrt (n,m));

            thus y in t by A5, Def4;

            thus thesis by A7, A8, Lm7;

          end;

            suppose

             A9: n >= mX;

            take y = ( PFArt (mX,m));

            thus y in t by A5, A9, Def4;

            thus thesis by A6, TARSKI:def 1;

          end;

        end;

        hence Sum <= t by Th12;

      end;

      then

       A10: ( PFDrt m) is_>=_than b by A1, Th31;

      

       A11: a <> b

      proof

        

         A12: ( PFArt (mX,m)) in Sum by TARSKI:def 1;

        assume

         A13: a = b;

        then Sum <= a by YELLOW_0: 24;

        then

        consider g be set such that

         A14: g in a and

         A15: g c= ( PFArt (mX,m)) by A12, Th12;

        per cases ;

          suppose g is non empty;

          then

          consider n be Element of NAT such that

           A16: [n, m] in g and

           A17: n is even by A1, A14, Th30;

          now

            per cases by A15, A16, Def2;

              suppose ex m9 be odd Element of NAT st m9 <= (2 * mX) & [m9, m] = [n, m];

              hence thesis by A17, XTUPLE_0: 1;

            end;

              suppose [(2 * mX), m] = [n, m];

              hence thesis by A14, A16, Th35, XREAL_1: 155;

            end;

          end;

          hence thesis;

        end;

          suppose

           A18: g is empty;

          reconsider P1 = ( PFBrt (1,m)) as Element of ( SubstPoset ( NAT , {m})) by Th25;

          ( PFBrt (1,m)) in ( PFDrt m) by Def5;

          then

           A19: P1 >= b by A10;

          ( PFBrt (1,m)) <> { {} } by Th27;

          hence thesis by A13, A14, A18, A19, Th32, Th38;

        end;

      end;

      a <= b by YELLOW_0: 22;

      then a < b by A11, ORDERS_2:def 6;

      hence contradiction by A2, A10, ORDERS_2: 6;

    end;

    registration

      let m be Element of NAT ;

      cluster ( SubstPoset ( NAT , {m})) -> non complete;

      coherence by Lm10;

    end

    registration

      let m be Element of NAT ;

      cluster ( SubstLatt ( NAT , {m})) -> non complete;

      coherence

      proof

        assume ( SubstLatt ( NAT , {m})) is complete;

        then

        reconsider K = ( SubstLatt ( NAT , {m})) as complete Lattice;

        ( LattPOSet K) is complete & ( SubstPoset ( NAT , {m})) is non complete;

        hence thesis;

      end;

    end