heyting1.miz

    begin

    theorem :: HEYTING1:1



     Th1: for A,B,C be non empty set, f be Function of A, B st for x be Element of A holds (f . x) in C holds f is Function of A, C

    proof

      let A,B,C be non empty set, f be Function of A, B;

      assume for x be Element of A holds (f . x) in C;

      then ( dom f) = A & for x be object holds x in A implies (f . x) in C by FUNCT_2:def 1;

      hence thesis by FUNCT_2: 3;

    end;

    reserve A for non empty set,

a for Element of A;

    definition

      let A;

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

      :: original: c=

      redefine

      :: HEYTING1:def1

      pred B c= C means for a st a in B holds a in C;

      compatibility

      proof

        thus B c= C implies for a st a in B holds a in C;

        assume

         A1: for a st a in B holds a in C;

        let x be object;

        assume

         A2: x in B;

        then x is Element of A by SETWISEO: 9;

        hence thesis by A1, A2;

      end;

    end

    reserve A for set;

    definition

      let A;

      assume

       A1: A is non empty;

      :: HEYTING1:def2

      func [A] -> non empty set equals

      : Def2: A;

      correctness by A1;

    end

    reserve B,C for Element of ( Fin ( DISJOINT_PAIRS A)),

x for Element of [:( Fin A), ( Fin A):],

a,b,c,d,s,t,s9,t9,t1,t2,s1,s2 for Element of ( DISJOINT_PAIRS A),

u,v,w for Element of ( NormForm A);

    theorem :: HEYTING1:2

    B = {} implies ( mi B) = {} by NORMFORM: 40, XBOOLE_1: 3;

     Lm1:

    now

      let A, a;

      reconsider B = {.a.} as Element of ( Fin ( DISJOINT_PAIRS A));

      now

        let c, b such that

         A1: c in B and

         A2: b in B and c c= b;

        c = a by A1, TARSKI:def 1;

        hence c = b by A2, TARSKI:def 1;

      end;

      hence {a} is Element of ( Normal_forms_on A) by NORMFORM: 33;

    end;

    registration

      let A;

      cluster non empty for Element of ( Normal_forms_on A);

      existence

      proof

        set a = the Element of ( DISJOINT_PAIRS A);

         {a} is Element of ( Normal_forms_on A) by Lm1;

        hence thesis;

      end;

    end

    definition

      let A, a;

      :: original: {

      redefine

      func {a} -> Element of ( Normal_forms_on A) ;

      coherence by Lm1;

    end

    definition

      let A;

      let u be Element of ( NormForm A);

      :: HEYTING1:def3

      func @ u -> Element of ( Normal_forms_on A) equals u;

      coherence by NORMFORM:def 12;

    end

    reserve K,L for Element of ( Normal_forms_on A);

    theorem :: HEYTING1:3



     Th3: ( mi (K ^ K)) = K

    proof



      thus ( mi (K ^ K)) = ( mi K) by NORMFORM: 55

      .= K by NORMFORM: 42;

    end;

    theorem :: HEYTING1:4



     Th4: for X be set st X c= K holds X in ( Normal_forms_on A)

    proof

      let X be set;

      assume

       A1: X c= K;

      K c= ( DISJOINT_PAIRS A) by FINSUB_1:def 5;

      then X c= ( DISJOINT_PAIRS A) by A1;

      then

      reconsider B = X as Element of ( Fin ( DISJOINT_PAIRS A)) by A1, FINSUB_1:def 5;

      for a, b st a in B & b in B & a c= b holds a = b by A1, NORMFORM: 32;

      hence thesis;

    end;

    theorem :: HEYTING1:5



     Th5: for X be set st X c= u holds X is Element of ( NormForm A)

    proof

      let X be set;

      assume

       A1: X c= u;

      u = ( @ u);

      then X in ( Normal_forms_on A) by A1, Th4;

      hence thesis by NORMFORM:def 12;

    end;

    definition

      let A;

      :: HEYTING1:def4

      func Atom (A) -> Function of ( DISJOINT_PAIRS A), the carrier of ( NormForm A) means

      : Def4: (it . a) = {a};

      existence

      proof

        set f = ( singleton ( DISJOINT_PAIRS A));



         A1: ( dom f) = ( DISJOINT_PAIRS A) by FUNCT_2:def 1;



         A2: the carrier of ( NormForm A) = ( Normal_forms_on A) by NORMFORM:def 12;

        now

          let x be object;

          assume x in ( DISJOINT_PAIRS A);

          then

          reconsider a = x as Element of ( DISJOINT_PAIRS A);

          (f . a) = {a} by SETWISEO: 54;

          hence (f . x) in the carrier of ( NormForm A) by A2;

        end;

        then

        reconsider f as Function of ( DISJOINT_PAIRS A), the carrier of ( NormForm A) by A1, FUNCT_2: 3;

        take f;

        thus thesis by SETWISEO: 54;

      end;

      uniqueness

      proof

        let IT1,IT2 be Function of ( DISJOINT_PAIRS A), the carrier of ( NormForm A) such that

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

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

        now

          let a;

          (IT1 . a) = {a} by A3;

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

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: HEYTING1:6



     Th6: c in (( Atom A) . a) implies c = a

    proof

      (( Atom A) . a) = {a} by Def4;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: HEYTING1:7



     Th7: a in (( Atom A) . a)

    proof

      (( Atom A) . a) = {a} by Def4;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: HEYTING1:8

    (( Atom A) . a) = (( singleton ( DISJOINT_PAIRS A)) . a)

    proof



      thus (( singleton ( DISJOINT_PAIRS A)) . a) = {a} by SETWISEO: 54

      .= (( Atom A) . a) by Def4;

    end;

    theorem :: HEYTING1:9



     Th9: ( FinJoin (K,( Atom A))) = ( FinUnion (K,( singleton ( DISJOINT_PAIRS A))))

    proof

      deffunc F( Element of ( Fin ( DISJOINT_PAIRS A))) = ( mi $1);



       A1: ( FinUnion (K,( singleton ( DISJOINT_PAIRS A)))) c= ( mi ( FinUnion (K,( singleton ( DISJOINT_PAIRS A)))))

      proof

        let a;

        assume

         A2: a in ( FinUnion (K,( singleton ( DISJOINT_PAIRS A))));

        then

        consider b such that

         A3: b in K and

         A4: a in (( singleton ( DISJOINT_PAIRS A)) . b) by SETWISEO: 57;



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

        now

          let s;

          assume that

           A6: s in ( FinUnion (K,( singleton ( DISJOINT_PAIRS A)))) and

           A7: s c= a;

          consider t such that

           A8: t in K and

           A9: s in (( singleton ( DISJOINT_PAIRS A)) . t) by A6, SETWISEO: 57;

          s = t by A9, SETWISEO: 55;

          hence s = a by A3, A5, A7, A8, NORMFORM: 32;

        end;

        hence thesis by A2, NORMFORM: 39;

      end;



       A10: ( mi ( FinUnion (K,( singleton ( DISJOINT_PAIRS A))))) c= ( FinUnion (K,( singleton ( DISJOINT_PAIRS A)))) by NORMFORM: 40;

      consider g be Function of ( Fin ( DISJOINT_PAIRS A)), ( Normal_forms_on A) such that

       A11: (g . B) = F(B) from FUNCT_2:sch 4;

      reconsider g as Function of ( Fin ( DISJOINT_PAIRS A)), the carrier of ( NormForm A) by NORMFORM:def 12;



       A12: (g . ( {}. ( DISJOINT_PAIRS A))) = ( mi ( {}. ( DISJOINT_PAIRS A))) by A11

      .= {} by NORMFORM: 40, XBOOLE_1: 3

      .= ( Bottom ( NormForm A)) by NORMFORM: 57

      .= ( the_unity_wrt the L_join of ( NormForm A)) by LATTICE2: 18;

       A13:

      now

        let x,y be Element of ( Fin ( DISJOINT_PAIRS A));



         A14: ( @ (g . x)) = ( mi x) & ( @ (g . y)) = ( mi y) by A11;



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

        .= ( mi (( mi x) \/ y)) by NORMFORM: 44

        .= ( mi (( mi x) \/ ( mi y))) by NORMFORM: 45

        .= (the L_join of ( NormForm A) . ((g . x),(g . y))) by A14, NORMFORM:def 12;

      end;

       A15:

      now

        let a;



        thus ((g * ( singleton ( DISJOINT_PAIRS A))) . a) = (g . (( singleton ( DISJOINT_PAIRS A)) . a)) by FUNCT_2: 15

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

        .= ( mi {a}) by A11

        .= {a} by NORMFORM: 42

        .= (( Atom A) . a) by Def4;

      end;



      thus ( FinJoin (K,( Atom A))) = (the L_join of ( NormForm A) $$ (K,( Atom A))) by LATTICE2:def 3

      .= (the L_join of ( NormForm A) $$ (K,(g * ( singleton ( DISJOINT_PAIRS A))))) by A15, FUNCT_2: 63

      .= (g . ( FinUnion (K,( singleton ( DISJOINT_PAIRS A))))) by A12, A13, SETWISEO: 53

      .= ( mi ( FinUnion (K,( singleton ( DISJOINT_PAIRS A))))) by A11

      .= ( FinUnion (K,( singleton ( DISJOINT_PAIRS A)))) by A10, A1;

    end;

    theorem :: HEYTING1:10



     Th10: u = ( FinJoin (( @ u),( Atom A)))

    proof



      thus u = ( FinUnion (( @ u),( singleton ( DISJOINT_PAIRS A)))) by SETWISEO: 58

      .= ( FinJoin (( @ u),( Atom A))) by Th9;

    end;



     Lm2: u [= v implies for x st x in u holds ex b st b in v & b c= x

    proof

      assume u [= v;



      then

       A1: v = (u "\/" v) by LATTICES:def 3

      .= (the L_join of ( NormForm A) . (u,v)) by LATTICES:def 1

      .= ( mi (( @ u) \/ ( @ v))) by NORMFORM:def 12;

      let x;

      assume

       A2: x in u;

      u = ( @ u);

      then

      reconsider c = x as Element of ( DISJOINT_PAIRS A) by A2, SETWISEO: 9;

      c in (u \/ v) by A2, XBOOLE_0:def 3;

      then

      consider b such that

       A3: b c= c & b in ( mi (( @ u) \/ ( @ v))) by NORMFORM: 41;

      take b;

      thus thesis by A1, A3;

    end;



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

    proof

      assume

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



       A2: ( mi (( @ u) \/ ( @ v))) c= ( @ v)

      proof

        let a;

        assume

         A3: a in ( mi (( @ u) \/ ( @ v)));

        then a in (u \/ v) by NORMFORM: 36;

        then a in u or a in v by XBOOLE_0:def 3;

        then

        consider b such that

         A4: b in v and

         A5: b c= a by A1;

        b in (u \/ v) by A4, XBOOLE_0:def 3;

        hence thesis by A3, A4, A5, NORMFORM: 38;

      end;



       A6: ( @ v) c= ( mi (( @ u) \/ ( @ v)))

      proof

        let a;

        assume

         A7: a in ( @ v);

        then

         A8: a in ( mi ( @ v)) by NORMFORM: 42;

         A9:

        now

          let b;

          assume that

           A10: b in (u \/ v) and

           A11: b c= a;

          b in u or b in v by A10, XBOOLE_0:def 3;

          then

          consider c such that

           A12: c in v and

           A13: c c= b by A1;

          c = a by A8, A11, A12, A13, NORMFORM: 2, NORMFORM: 38;

          hence b = a by A11, A13, NORMFORM: 1;

        end;

        a in (( @ u) \/ ( @ v)) by A7, XBOOLE_0:def 3;

        hence thesis by A9, NORMFORM: 39;

      end;

      (u "\/" v) = (the L_join of ( NormForm A) . (u,v)) by LATTICES:def 1

      .= ( mi (( @ u) \/ ( @ v))) by NORMFORM:def 12

      .= v by A2, A6;

      hence thesis by LATTICES:def 3;

    end;

    reserve f,f9 for Element of ( Funcs (( DISJOINT_PAIRS A), [:( Fin A), ( Fin A):])),

g,h for Element of ( Funcs (( DISJOINT_PAIRS A), [A]));

    definition

      let A be set;

      :: HEYTING1:def5

      func pair_diff A -> BinOp of [:( Fin A), ( Fin A):] means

      : Def5: for a,b be Element of [:( Fin A), ( Fin A):] holds (it . (a,b)) = (a \ b);

      existence

      proof

        deffunc F( Element of [:( Fin A), ( Fin A):], Element of [:( Fin A), ( Fin A):]) = ($1 \ $2);

        thus ex f be BinOp of [:( Fin A), ( Fin A):] st for a,b be Element of [:( Fin A), ( Fin A):] holds (f . (a,b)) = F(a,b) from BINOP_1:sch 4;

      end;

      correctness

      proof

        let IT,IT9 be BinOp of [:( Fin A), ( Fin A):] such that

         A1: for a,b be Element of [:( Fin A), ( Fin A):] holds (IT . (a,b)) = (a \ b) and

         A2: for a,b be Element of [:( Fin A), ( Fin A):] holds (IT9 . (a,b)) = (a \ b);

        now

          let a,b be Element of [:( Fin A), ( Fin A):];

          (IT . (a,b)) = (a \ b) by A1;

          hence (IT . (a,b)) = (IT9 . (a,b)) by A2;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    definition

      let A, B;

      :: HEYTING1:def6

      func - B -> Element of ( Fin ( DISJOINT_PAIRS A)) equals (( DISJOINT_PAIRS A) /\ { [{ (g . t1) : (g . t1) in (t1 `2 ) & t1 in B }, { (g . t2) : (g . t2) in (t2 `1 ) & t2 in B }] : s in B implies (g . s) in ((s `1 ) \/ (s `2 )) });

      coherence

      proof

        deffunc G( set) = (($1 `1 ) \/ ($1 `2 ));

        defpred Q[ Function] means ($1 .: B) c= ( union { ((s `1 ) \/ (s `2 )) : s in B });

        defpred P[ Function] means s in B implies ($1 . s) in ((s `1 ) \/ (s `2 ));

        deffunc F( Element of ( Funcs (( DISJOINT_PAIRS A), [A]))) = [{ ($1 . s1) : ($1 . s1) in (s1 `2 ) & s1 in B }, { ($1 . s2) : ($1 . s2) in (s2 `1 ) & s2 in B }];

        set N = { F(g) : s in B implies (g . s) in ((s `1 ) \/ (s `2 )) };

        set N9 = { F(g) : (g .: B) c= ( union { ((s `1 ) \/ (s `2 )) : s in B }) };

        set M = (( DISJOINT_PAIRS A) /\ N);

         A1:

        now

          let X be set;

          assume X in { ((s `1 ) \/ (s `2 )) : s in B };

          then ex s st X = ((s `1 ) \/ (s `2 )) & s in B;

          hence X is finite;

        end;

         A2:

        now

          let g, h;

          defpred P1[ set] means (g . $1) in ($1 `1 );

          defpred P2[ set] means (g . $1) in ($1 `2 );

          defpred Q1[ set] means (h . $1) in ($1 `1 );

          defpred Q2[ set] means (h . $1) in ($1 `2 );

          assume

           A3: (g | B) = (h | B);

          then

           A4: for s st s in B holds P1[s] iff Q1[s] by FRAENKEL: 1;



           A5: { (g . s2) where s2 be Element of ( DISJOINT_PAIRS A) : P1[s2] & s2 in B } = { (h . t2) where t2 be Element of ( DISJOINT_PAIRS A) : Q1[t2] & t2 in B } from FRAENKEL:sch 9( A3, A4);



           A6: for s st s in B holds P2[s] iff Q2[s] by A3, FRAENKEL: 1;

          { (g . s1) where s1 be Element of ( DISJOINT_PAIRS A) : P2[s1] & s1 in B } = { (h . t1) where t1 be Element of ( DISJOINT_PAIRS A) : Q2[t1] & t1 in B } from FRAENKEL:sch 9( A3, A6);

          hence F(g) = F(h) by A5;

        end;



         A7: for g holds P[g] implies Q[g]

        proof

          let g such that

           A8: for s holds s in B implies (g . s) in ((s `1 ) \/ (s `2 ));

          let x be object;

          assume x in (g .: B);

          then

          consider y be object such that

           A9: y in ( dom g) and

           A10: y in B and

           A11: x = (g . y) by FUNCT_1:def 6;

          reconsider y as Element of ( DISJOINT_PAIRS A) by A9;



           A12: ((y `1 ) \/ (y `2 )) in { ((s `1 ) \/ (s `2 )) : s in B } by A10;

          (g . y) in ((y `1 ) \/ (y `2 )) by A8, A10;

          hence thesis by A11, A12, TARSKI:def 4;

        end;



         A13: { F(g) where g be Element of ( Funcs (( DISJOINT_PAIRS A), [A])) : P[g] } c= { F(g) where g be Element of ( Funcs (( DISJOINT_PAIRS A), [A])) : Q[g] } from FRAENKEL:sch 1( A7);



         A14: B is finite;

        { G(s) : s in B } is finite from FRAENKEL:sch 21( A14);

        then

         A15: ( union { ((s `1 ) \/ (s `2 )) : s in B }) is finite by A1, FINSET_1: 7;



         A16: N9 is finite from FRAENKEL:sch 25( A14, A15, A2);

        M c= ( DISJOINT_PAIRS A) by XBOOLE_1: 17;

        hence thesis by A13, A16, FINSUB_1:def 5;

      end;

      correctness ;

      let C;

      :: HEYTING1:def7

      func B =>> C -> Element of ( Fin ( DISJOINT_PAIRS A)) equals (( DISJOINT_PAIRS A) /\ { ( FinPairUnion (B,(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))))) : (f .: B) c= C });

      coherence

      proof

        deffunc F( Element of ( Funcs (( DISJOINT_PAIRS A), [:( Fin A), ( Fin A):]))) = ( FinPairUnion (B,(( pair_diff A) .: ($1,( incl ( DISJOINT_PAIRS A))))));

        set N = { ( FinPairUnion (B,(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))))) : (f .: B) c= C };

        set IT = (( DISJOINT_PAIRS A) /\ N);



         A17: IT c= ( DISJOINT_PAIRS A) by XBOOLE_1: 17;

         A18:

        now

          let f, f9;

          assume (f | B) = (f9 | B);

          then ((( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))) | B) = ((( pair_diff A) .: (f9,( incl ( DISJOINT_PAIRS A)))) | B) by FUNCOP_1: 23;

          hence F(f) = F(f9) by NORMFORM: 22;

        end;



         A19: C is finite;



         A20: B is finite;

        { F(f) : (f .: B) c= C } is finite from FRAENKEL:sch 25( A20, A19, A18);

        hence thesis by A17, FINSUB_1:def 5;

      end;

      correctness ;

    end

    theorem :: HEYTING1:11



     Th11: c in ( - B) implies ex g st (for s st s in B holds (g . s) in ((s `1 ) \/ (s `2 ))) & c = [{ (g . t1) : (g . t1) in (t1 `2 ) & t1 in B }, { (g . t2) : (g . t2) in (t2 `1 ) & t2 in B }]

    proof

      assume c in ( - B);

      then c in { [{ (g . t1) : (g . t1) in (t1 `2 ) & t1 in B }, { (g . t2) : (g . t2) in (t2 `1 ) & t2 in B }] : s in B implies (g . s) in ((s `1 ) \/ (s `2 )) } by XBOOLE_0:def 4;

      then ex g st c = [{ (g . t1) : (g . t1) in (t1 `2 ) & t1 in B }, { (g . t2) : (g . t2) in (t2 `1 ) & t2 in B }] & for s st s in B holds (g . s) in ((s `1 ) \/ (s `2 ));

      hence thesis;

    end;

    theorem :: HEYTING1:12



     Th12: [ {} , {} ] is Element of ( DISJOINT_PAIRS A)

    proof

       [ {} , {} ] = [( {}. A), ( {}. A)] & ( [ {} , {} ] `1 ) misses ( [ {} , {} ] `2 );

      hence thesis by NORMFORM: 29;

    end;

    theorem :: HEYTING1:13



     Th13: for K st K = {} holds ( - K) = { [ {} , {} ]}

    proof

      let K;

      assume

       A1: K = {} ;



       A2: { [{ (g . t1) : (g . t1) in (t1 `2 ) & t1 in K }, { (g . t2) : (g . t2) in (t2 `1 ) & t2 in K }] : s in K implies (g . s) in ((s `1 ) \/ (s `2 )) } = { [ {} , {} ]}

      proof

        thus { [{ (g . t1) : (g . t1) in (t1 `2 ) & t1 in K }, { (g . t2) : (g . t2) in (t2 `1 ) & t2 in K }] : s in K implies (g . s) in ((s `1 ) \/ (s `2 )) } c= { [ {} , {} ]}

        proof

          let x be object;

          assume x in { [{ (g . t1) : (g . t1) in (t1 `2 ) & t1 in K }, { (g . t2) : (g . t2) in (t2 `1 ) & t2 in K }] : s in K implies (g . s) in ((s `1 ) \/ (s `2 )) };

          then

          consider g such that

           A3: x = [{ (g . t1) : (g . t1) in (t1 `2 ) & t1 in K }, { (g . t2) : (g . t2) in (t2 `1 ) & t2 in K }] and s in K implies (g . s) in ((s `1 ) \/ (s `2 ));



           A4: (x `2 ) = { (g . t2) : (g . t2) in (t2 `1 ) & t2 in K } by A3;

           A5:

          now

            set y = the Element of (x `2 );

            assume (x `2 ) <> {} ;

            then y in (x `2 );

            then ex t1 st y = (g . t1) & (g . t1) in (t1 `1 ) & t1 in K by A4;

            hence contradiction by A1;

          end;



           A6: (x `1 ) = { (g . t1) : (g . t1) in (t1 `2 ) & t1 in K } by A3;

          now

            set y = the Element of (x `1 );

            assume (x `1 ) <> {} ;

            then y in (x `1 );

            then ex t1 st y = (g . t1) & (g . t1) in (t1 `2 ) & t1 in K by A6;

            hence contradiction by A1;

          end;

          then x = [ {} , {} ] by A3, A5;

          hence thesis by TARSKI:def 1;

        end;

        thus { [ {} , {} ]} c= { [{ (g . t1) : (g . t1) in (t1 `2 ) & t1 in K }, { (g . t2) : (g . t2) in (t2 `1 ) & t2 in K }] : s in K implies (g . s) in ((s `1 ) \/ (s `2 )) }

        proof

          set g = the Element of ( Funcs (( DISJOINT_PAIRS A), [A]));

          let x be object;

          assume x in { [ {} , {} ]};

          then

           A7: x = [ {} , {} ] by TARSKI:def 1;

           A8:

          now

            set y = the Element of { (g . t1) : (g . t1) in (t1 `2 ) & t1 in K };

            assume { (g . t1) : (g . t1) in (t1 `2 ) & t1 in K } <> {} ;

            then y in { (g . t1) : (g . t1) in (t1 `2 ) & t1 in K };

            then ex t1 st y = (g . t1) & (g . t1) in (t1 `2 ) & t1 in K;

            hence contradiction by A1;

          end;

           A9:

          now

            set y = the Element of { (g . t2) : (g . t2) in (t2 `1 ) & t2 in K };

            assume { (g . t2) : (g . t2) in (t2 `1 ) & t2 in K } <> {} ;

            then y in { (g . t2) : (g . t2) in (t2 `1 ) & t2 in K };

            then ex t1 st y = (g . t1) & (g . t1) in (t1 `1 ) & t1 in K;

            hence contradiction by A1;

          end;

          s in K implies (g . s) in ((s `1 ) \/ (s `2 )) by A1;

          hence thesis by A7, A8, A9;

        end;

      end;

       [ {} , {} ] is Element of ( DISJOINT_PAIRS A) by Th12;

      hence thesis by A2, ZFMISC_1: 46;

    end;

    theorem :: HEYTING1:14



     Th14: for K, L st K = {} & L = {} holds (K =>> L) = { [ {} , {} ]}

    proof

      let K, L;

      assume that

       A1: K = {} and L = {} ;



       A2: {} = ( {}. A);



       A3: K = ( {}. ( DISJOINT_PAIRS A)) by A1;

       A4:

      now

        let f;



        thus ( FinPairUnion (K,(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))))) = ( the_unity_wrt ( FinPairUnion A)) by A3, NORMFORM: 18, SETWISEO: 31

        .= [ {} , {} ] by A2, NORMFORM: 19;

      end;



       A5: { ( FinPairUnion (K,(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))))) : (f .: K) c= L } = { [ {} , {} ]}

      proof

        thus { ( FinPairUnion (K,(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))))) : (f .: K) c= L } c= { [ {} , {} ]}

        proof

          let x be object;

          assume x in { ( FinPairUnion (K,(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))))) : (f .: K) c= L };

          then ex f st x = ( FinPairUnion (K,(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))))) & (f .: K) c= L;

          then x = [ {} , {} ] by A4;

          hence thesis by TARSKI:def 1;

        end;

        thus { [ {} , {} ]} c= { ( FinPairUnion (K,(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))))) : (f .: K) c= L }

        proof

          set f9 = the Element of ( Funcs (( DISJOINT_PAIRS A), [:( Fin A), ( Fin A):]));

          let x be object;

          assume x in { [ {} , {} ]};

          then x = [ {} , {} ] by TARSKI:def 1;

          then

           A6: x = ( FinPairUnion (K,(( pair_diff A) .: (f9,( incl ( DISJOINT_PAIRS A)))))) by A4;

          (f9 .: K) c= L by A1;

          hence thesis by A6;

        end;

      end;

       [ {} , {} ] is Element of ( DISJOINT_PAIRS A) by Th12;

      hence thesis by A5, ZFMISC_1: 46;

    end;

    theorem :: HEYTING1:15



     Th15: for a be Element of ( DISJOINT_PAIRS {} ) holds a = [ {} , {} ]

    proof

      let a be Element of ( DISJOINT_PAIRS {} );

      consider x,y be Element of ( Fin {} ) such that

       A1: a = [x, y] by DOMAIN_1: 1;

      x = {} by FINSUB_1: 15, TARSKI:def 1;

      hence thesis by A1, FINSUB_1: 15, TARSKI:def 1;

    end;

    theorem :: HEYTING1:16



     Th16: ( DISJOINT_PAIRS {} ) = { [ {} , {} ]}

    proof

      thus ( DISJOINT_PAIRS {} ) c= { [ {} , {} ]}

      proof

        let x be object;

        assume x in ( DISJOINT_PAIRS {} );

        then x = [ {} , {} ] by Th15;

        hence thesis by TARSKI:def 1;

      end;

      thus { [ {} , {} ]} c= ( DISJOINT_PAIRS {} )

      proof

        let x be object;

        assume x in { [ {} , {} ]};

        then x = [ {} , {} ] by TARSKI:def 1;

        then x is Element of ( DISJOINT_PAIRS {} ) by Th12;

        hence thesis;

      end;

    end;



     Lm4: ( Fin ( DISJOINT_PAIRS {} )) = { {} , { [ {} , {} ]}}

    proof



      thus ( Fin ( DISJOINT_PAIRS {} )) = ( bool ( DISJOINT_PAIRS {} )) by Th16, FINSUB_1: 14

      .= { {} , { [ {} , {} ]}} by Th16, ZFMISC_1: 24;

    end;

    theorem :: HEYTING1:17



     Th17: { [ {} , {} ]} is Element of ( Normal_forms_on A)

    proof

       [ {} , {} ] is Element of ( DISJOINT_PAIRS A) by Th12;

      then { [ {} , {} ]} c= ( DISJOINT_PAIRS A) by ZFMISC_1: 31;

      then

      reconsider B = { [ {} , {} ]} as Element of ( Fin ( DISJOINT_PAIRS A)) by FINSUB_1:def 5;

      now

        let a,b be Element of ( DISJOINT_PAIRS A);

        assume that

         A1: a in B and

         A2: b in B and a c= b;

        a = [ {} , {} ] by A1, TARSKI:def 1;

        hence a = b by A2, TARSKI:def 1;

      end;

      hence thesis by NORMFORM: 33;

    end;

    theorem :: HEYTING1:18



     Th18: c in (B =>> C) implies ex f st (f .: B) c= C & c = ( FinPairUnion (B,(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A))))))

    proof

      assume c in (B =>> C);

      then c in { ( FinPairUnion (B,(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))))) : (f .: B) c= C } by XBOOLE_0:def 4;

      then ex f st c = ( FinPairUnion (B,(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))))) & (f .: B) c= C;

      hence thesis;

    end;

    theorem :: HEYTING1:19



     Th19: (K ^ {a}) = {} implies ex b st b in ( - K) & b c= a

    proof

      assume

       A1: (K ^ {a}) = {} ;

      now

        per cases ;

          suppose

           A2: A is non empty;

          defpred P[ set, set] means $2 in ((($1 `1 ) /\ (a `2 )) \/ (($1 `2 ) /\ (a `1 )));



           A3: A = [A] by A2, Def2;

           A4:

          now



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

            let s;

            assume s in K;

            then not (s \/ a) in ( DISJOINT_PAIRS A) by A1, A5, NORMFORM: 35;

            then

            consider x be Element of [A] such that

             A6: x in (s `1 ) & x in (a `2 ) or x in (a `1 ) & x in (s `2 ) by A3, NORMFORM: 28;

            take x;

            x in ((s `1 ) /\ (a `2 )) or x in ((s `2 ) /\ (a `1 )) by A6, XBOOLE_0:def 4;

            hence P[s, x] by XBOOLE_0:def 3;

          end;

          consider g such that

           A7: s in K implies P[s, (g . s)] from FRAENKEL:sch 27( A4);

          set c1 = { (g . t1) : (g . t1) in (t1 `2 ) & t1 in K }, c2 = { (g . t2) : (g . t2) in (t2 `1 ) & t2 in K };



           A8: c2 c= (a `2 )

          proof

            let x be object;

            assume x in c2;

            then

            consider t such that

             A9: x = (g . t) & (g . t) in (t `1 ) and

             A10: t in K;

            (g . t) in (((t `1 ) /\ (a `2 )) \/ ((t `2 ) /\ (a `1 ))) by A7, A10;

            then (g . t) in ((t `1 ) /\ (a `2 )) or (g . t) in ((t `2 ) /\ (a `1 )) by XBOOLE_0:def 3;

            then (g . t) in (t `1 ) & (g . t) in (a `2 ) or (g . t) in (t `2 ) & (g . t) in (a `1 ) by XBOOLE_0:def 4;

            hence thesis by A9, NORMFORM: 27;

          end;



           A11: c1 c= (a `1 )

          proof

            let x be object;

            assume x in c1;

            then

            consider t such that

             A12: x = (g . t) & (g . t) in (t `2 ) and

             A13: t in K;

            (g . t) in (((t `1 ) /\ (a `2 )) \/ ((t `2 ) /\ (a `1 ))) by A7, A13;

            then (g . t) in ((t `1 ) /\ (a `2 )) or (g . t) in ((t `2 ) /\ (a `1 )) by XBOOLE_0:def 3;

            then (g . t) in (t `1 ) & (g . t) in (a `2 ) or (g . t) in (t `2 ) & (g . t) in (a `1 ) by XBOOLE_0:def 4;

            hence thesis by A12, NORMFORM: 27;

          end;

          then

          reconsider c = [c1, c2] as Element of ( DISJOINT_PAIRS A) by A8, NORMFORM: 30;

          take c;

          now

            let s;

            assume s in K;

            then (g . s) in (((s `1 ) /\ (a `2 )) \/ ((s `2 ) /\ (a `1 ))) by A7;

            then (g . s) in ((s `1 ) /\ (a `2 )) or (g . s) in ((s `2 ) /\ (a `1 )) by XBOOLE_0:def 3;

            then (g . s) in (s `1 ) & (g . s) in (a `2 ) or (g . s) in (s `2 ) & (g . s) in (a `1 ) by XBOOLE_0:def 4;

            hence (g . s) in ((s `1 ) \/ (s `2 )) by XBOOLE_0:def 3;

          end;

          then c in { [{ (h . t1) : (h . t1) in (t1 `2 ) & t1 in K }, { (h . t2) : (h . t2) in (t2 `1 ) & t2 in K }] : s in K implies (h . s) in ((s `1 ) \/ (s `2 )) };

          hence c in ( - K) by XBOOLE_0:def 4;

          thus c c= a by A11, A8;

        end;

          suppose

           A14: not A is non empty;

          reconsider Z = { [ {} , {} ]} as Element of ( Normal_forms_on {} ) by Th17;

          take b = a;



           A15: a = [ {} , {} ] by A14, Th15;

          ( mi (Z ^ Z)) <> {} by Th3;

          then K <> { [ {} , {} ]} by A1, A14, A15, NORMFORM: 40, XBOOLE_1: 3;

          then K = {} by A14, Lm4, TARSKI:def 2;

          then ( - K) = { [ {} , {} ]} by Th13;

          hence b in ( - K) by A15, TARSKI:def 1;

          thus b c= a;

        end;

      end;

      hence thesis;

    end;

     Lm5:

    now

      let A, K, b, f;



      thus ((( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))) . b) = (( pair_diff A) . ((f . b),(( incl ( DISJOINT_PAIRS A)) . b))) by FUNCOP_1: 37

      .= (( pair_diff A) . ((f . b),b)) by FUNCT_1: 18

      .= ((f . b) \ b) by Def5;

    end;

    theorem :: HEYTING1:20



     Th20: (for c st c in u holds ex b st b in v & b c= (c \/ a)) implies ex b st b in (( @ u) =>> ( @ v)) & b c= a

    proof

      defpred P[ Element of ( DISJOINT_PAIRS A), Element of [:( Fin A), ( Fin A):]] means $2 in ( @ v) & $2 c= ($1 \/ a);

      assume

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

       A2:

      now

        let b;

        assume b in ( @ u);

        then

        consider c such that

         A3: c in v & c c= (b \/ a) by A1;

        reconsider c as Element of [:( Fin A), ( Fin A):];

        take x = c;

        thus P[b, x] by A3;

      end;

      consider f9 such that

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

      set d = ( FinPairUnion (( @ u),(( pair_diff A) .: (f9,( incl ( DISJOINT_PAIRS A))))));

       A5:

      now

        let s;

        assume s in u;

        then

         A6: (f9 . s) c= (a \/ s) by A4;

        ((( pair_diff A) .: (f9,( incl ( DISJOINT_PAIRS A)))) . s) = ((f9 . s) \ s) by Lm5;

        hence ((( pair_diff A) .: (f9,( incl ( DISJOINT_PAIRS A)))) . s) c= a by A6, NORMFORM: 15;

      end;

      then

      reconsider d as Element of ( DISJOINT_PAIRS A) by NORMFORM: 21, NORMFORM: 26;

      take d;

      b in u implies (f9 . b) in v by A4;

      then (f9 .: ( @ u)) c= v by SETWISEO: 10;

      then d in { ( FinPairUnion (( @ u),(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))))) : (f .: ( @ u)) c= v };

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

      thus thesis by A5, NORMFORM: 21;

    end;



     Lm6: a in (K ^ (K =>> ( @ u))) implies ex b st b in u & b c= a

    proof

      assume a in (K ^ (K =>> ( @ u)));

      then

      consider b, c such that

       A1: b in K and

       A2: c in (K =>> ( @ u)) and

       A3: a = (b \/ c) by NORMFORM: 34;

      consider f such that

       A4: (f .: K) c= u and

       A5: c = ( FinPairUnion (K,(( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))))) by A2, Th18;



       A6: (f . b) in (f .: K) by A1, FUNCT_2: 35;

      u = ( @ u);

      then

      reconsider d = (f . b) as Element of ( DISJOINT_PAIRS A) by A4, A6, SETWISEO: 9;

      take d;

      thus d in u by A4, A6;

      ((( pair_diff A) .: (f,( incl ( DISJOINT_PAIRS A)))) . b) = ((f . b) \ b) by Lm5;

      hence thesis by A1, A3, A5, NORMFORM: 14, NORMFORM: 16;

    end;

    theorem :: HEYTING1:21



     Th21: (K ^ ( - K)) = {}

    proof

      set x = the Element of (K ^ ( - K));

      assume

       A1: (K ^ ( - K)) <> {} ;

      then

      reconsider a = x as Element of ( DISJOINT_PAIRS A) by SETWISEO: 9;

      consider b, c such that

       A2: b in K and

       A3: c in ( - K) and

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



       A5: (a `1 ) = ((b `1 ) \/ (c `1 )) by A4;



       A6: (a `2 ) = ((b `2 ) \/ (c `2 )) by A4;

      consider g such that

       A7: s in K implies (g . s) in ((s `1 ) \/ (s `2 )) and

       A8: c = [{ (g . t1) : (g . t1) in (t1 `2 ) & t1 in K }, { (g . t2) : (g . t2) in (t2 `1 ) & t2 in K }] by A3, Th11;



       A9: (g . b) in ((b `1 ) \/ (b `2 )) by A2, A7;

      now

        per cases by A9, XBOOLE_0:def 3;

          case

           A10: (g . b) in (b `1 );

          hence (g . b) in (a `1 ) by A5, XBOOLE_0:def 3;

          (g . b) in { (g . t2) : (g . t2) in (t2 `1 ) & t2 in K } by A2, A10;

          then (g . b) in (c `2 ) by A8;

          hence (g . b) in (a `2 ) by A6, XBOOLE_0:def 3;

        end;

          case

           A11: (g . b) in (b `2 );

          hence (g . b) in (a `2 ) by A6, XBOOLE_0:def 3;

          (g . b) in { (g . t1) : (g . t1) in (t1 `2 ) & t1 in K } by A2, A11;

          then (g . b) in (c `1 ) by A8;

          hence (g . b) in (a `1 ) by A5, XBOOLE_0:def 3;

        end;

      end;

      then ((a `1 ) /\ (a `2 )) <> {} by XBOOLE_0:def 4;

      then (a `1 ) meets (a `2 );

      hence contradiction by NORMFORM: 25;

    end;

    definition

      let A;

      :: HEYTING1:def8

      func pseudo_compl (A) -> UnOp of the carrier of ( NormForm A) means

      : Def8: (it . u) = ( mi ( - ( @ u)));

      existence

      proof

        deffunc F( Element of ( NormForm A)) = ( mi ( - ( @ $1)));

        consider IT be Function of the carrier of ( NormForm A), ( Normal_forms_on A) such that

         A1: (IT . u) = F(u) from FUNCT_2:sch 4;

        reconsider IT as UnOp of the carrier of ( NormForm A) by NORMFORM:def 12;

        take IT;

        let u;

        thus thesis by A1;

      end;

      correctness

      proof

        let IT,IT9 be UnOp of the carrier of ( NormForm A);

        assume that

         A2: (IT . u) = ( mi ( - ( @ u))) and

         A3: (IT9 . u) = ( mi ( - ( @ u)));

        now

          let u;



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

          .= (IT9 . u) by A3;

        end;

        hence IT = IT9 by FUNCT_2: 63;

      end;

      :: HEYTING1:def9

      func StrongImpl (A) -> BinOp of the carrier of ( NormForm A) means

      : Def9: (it . (u,v)) = ( mi (( @ u) =>> ( @ v)));

      existence

      proof

        deffunc F( Element of ( NormForm A), Element of ( NormForm A)) = ( mi (( @ $1) =>> ( @ $2)));

        consider IT be Function of [:the carrier of ( NormForm A), the carrier of ( NormForm A):], ( Normal_forms_on A) such that

         A4: (IT . (u,v)) = F(u,v) from BINOP_1:sch 4;

        reconsider IT as BinOp of the carrier of ( NormForm A) by NORMFORM:def 12;

        take IT;

        let u, v;

        thus thesis by A4;

      end;

      correctness

      proof

        let IT,IT9 be BinOp of the carrier of ( NormForm A);

        assume that

         A5: (IT . (u,v)) = ( mi (( @ u) =>> ( @ v))) and

         A6: (IT9 . (u,v)) = ( mi (( @ u) =>> ( @ v)));

        now

          let u, v;



          thus (IT . (u,v)) = ( mi (( @ u) =>> ( @ v))) by A5

          .= (IT9 . (u,v)) by A6;

        end;

        hence IT = IT9 by BINOP_1: 2;

      end;

      let u;

      :: HEYTING1:def10

      func SUB u -> Element of ( Fin the carrier of ( NormForm A)) equals ( bool u);

      coherence

      proof



         A7: ( bool u) c= the carrier of ( NormForm A)

        proof

          let x be object;

          assume x in ( bool u);

          then x is Element of ( NormForm A) by Th5;

          hence thesis;

        end;

        u = ( @ u);

        hence thesis by A7, FINSUB_1:def 5;

      end;

      correctness ;

      :: HEYTING1:def11

      func diff (u) -> UnOp of the carrier of ( NormForm A) means

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

      existence

      proof

        deffunc F( Element of ( NormForm A)) = (( @ u) \ ( @ $1));

        consider IT be Function of the carrier of ( NormForm A), ( Fin ( DISJOINT_PAIRS A)) such that

         A8: (IT . v) = F(v) from FUNCT_2:sch 4;

        now

          let v be Element of ( NormForm A);

          (( @ u) \ ( @ v)) in ( Normal_forms_on A) by Th4, XBOOLE_1: 36;

          then (IT . v) in ( Normal_forms_on A) by A8;

          hence (IT . v) in the carrier of ( NormForm A) by NORMFORM:def 12;

        end;

        then

        reconsider IT as UnOp of the carrier of ( NormForm A) by Th1;

        take IT;

        let v;

        v = ( @ v);

        hence thesis by A8;

      end;

      correctness

      proof

        let IT,IT9 be UnOp of the carrier of ( NormForm A);

        assume that

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

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

        now

          let v be Element of ( NormForm A);



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

          .= (IT9 . v) by A10;

        end;

        hence IT = IT9 by FUNCT_2: 63;

      end;

    end

    deffunc J( set) = the L_join of ( NormForm $1);

    deffunc M( set) = the L_meet of ( NormForm $1);



     Lm7: for u, v st v in ( SUB u) holds (v "\/" (( diff u) . v)) = u

    proof

      let u, v;

      assume

       A1: v in ( SUB u);



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



      thus (v "\/" (( diff u) . v)) = ( J(A) . (v,(( diff u) . v))) by LATTICES:def 1

      .= ( mi (( @ v) \/ (( @ u) \ ( @ v)))) by A2, NORMFORM:def 12

      .= ( mi ( @ u)) by A1, XBOOLE_1: 45

      .= u by NORMFORM: 42;

    end;

    theorem :: HEYTING1:22



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

    proof

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

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

      hence thesis by Lm3;

    end;



     Lm8: ex v st v in ( SUB u) & (( @ v) ^ {a}) = {} & for b st b in (( diff u) . v) holds (b \/ a) in ( DISJOINT_PAIRS A)

    proof

      defpred Q[ set] means not contradiction;

      deffunc F( set) = $1;

      defpred P[ Element of ( DISJOINT_PAIRS A)] means not ($1 \/ a) in ( DISJOINT_PAIRS A);

      set M = { F(s) : F(s) in u & P[s] };

      deffunc F1( Element of ( DISJOINT_PAIRS A)) = ($1 \/ a);

      defpred P1[ set] means $1 in u;

      defpred P2[ Element of ( DISJOINT_PAIRS A)] means P1[$1] & P[$1];



       A1: { F1(t) where t be Element of ( DISJOINT_PAIRS A) : t in { s where s be Element of ( DISJOINT_PAIRS A) : P2[s] } & Q[t] } = { F1(s) where s be Element of ( DISJOINT_PAIRS A) : P2[s] & Q[s] } from FRAENKEL:sch 14;

      defpred F[ set, set] means $1 in M;

      defpred D[ set, set] means $1 in M & $2 in {a};



       A2: { F1(s1) : P2[s1] & Q[s1] } = { F1(s2) : P2[s2] }

      proof

        thus { F1(s1) : P2[s1] & Q[s1] } c= { F1(s2) : P2[s2] }

        proof

          let x be object;

          assume x in { F1(s1) : P2[s1] & Q[s1] };

          then ex s1 st x = F1(s1) & P2[s1] & Q[s1];

          hence thesis;

        end;

        let x be object;

        assume x in { F1(s1) : P2[s1] };

        then ex s1 st x = F1(s1) & P2[s1];

        hence thesis;

      end;



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

      then

      reconsider v = M as Element of ( NormForm A) by Th5;

      take v;

      thus v in ( SUB u) by A3;

      defpred E[ set, set] means $2 = a & $1 in M;

      deffunc G( Element of ( DISJOINT_PAIRS A), Element of ( DISJOINT_PAIRS A)) = ($1 \/ $2);



       A4: { F1(t) : t in { s : P2[s] } & Q[t] } = { F1(t1) : t1 in { s1 : P2[s1] } }

      proof

        thus { F1(t) : t in { s : P2[s] } & Q[t] } c= { F1(t1) : t1 in { s1 : P2[s1] } }

        proof

          let x be object;

          assume x in { F1(t) : t in { s : P2[s] } & Q[t] };

          then ex t st x = F1(t) & t in { s : P2[s] } & Q[t];

          hence thesis;

        end;

        let x be object;

        assume x in { F1(t) : t in { s : P2[s] } };

        then ex t st x = F1(t) & t in { s : P2[s] };

        hence thesis;

      end;



       A5: { G(s,t) where t be Element of ( DISJOINT_PAIRS A) : t = a & F[s, t] } = { G(s9,a) : F[s9, a] } from FRAENKEL:sch 20;



       A6: D[s, t] iff E[s, t] by TARSKI:def 1;



       A7: { G(s,t) : D[s, t] } = { G(s9,t9) : E[s9, t9] } from FRAENKEL:sch 4( A6);

      { F1(s) : P1[s] & not F1(s) in ( DISJOINT_PAIRS A) } misses ( DISJOINT_PAIRS A) from FRAENKEL:sch 18;

      hence (( @ v) ^ {a}) = {} by A1, A4, A2, A7, A5;

      let b;

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

      then

       A8: b in (u \ v) by Def11;

      then not b in M by XBOOLE_0:def 5;

      hence thesis by A8;

    end;

    theorem :: HEYTING1:23



     Th23: (u "/\" (( pseudo_compl A) . u)) = ( Bottom ( NormForm A))

    proof

      reconsider zero = {} as Element of ( Normal_forms_on A) by NORMFORM: 31;



       A1: ( @ (( pseudo_compl A) . u)) = ( mi ( - ( @ u))) by Def8;



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

      .= ( mi (( @ u) ^ ( mi ( - ( @ u))))) by A1, NORMFORM:def 12

      .= ( mi (( @ u) ^ ( - ( @ u)))) by NORMFORM: 51

      .= ( mi zero) by Th21

      .= {} by NORMFORM: 40, XBOOLE_1: 3

      .= ( Bottom ( NormForm A)) by NORMFORM: 57;

    end;

    theorem :: HEYTING1:24



     Th24: (u "/\" (( StrongImpl A) . (u,v))) [= v

    proof

      now

        let a;

        assume

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



         A2: ( @ (( StrongImpl A) . (u,v))) = ( mi (( @ u) =>> ( @ v))) by Def9;

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

        .= ( mi (( @ u) ^ ( mi (( @ u) =>> ( @ v))))) by A2, NORMFORM:def 12

        .= ( mi (( @ u) ^ (( @ u) =>> ( @ v)))) by NORMFORM: 51;

        then a in (( @ u) ^ (( @ u) =>> ( @ v))) by A1, NORMFORM: 36;

        hence ex b st b in v & b c= a by Lm6;

      end;

      hence thesis by Lm3;

    end;

    theorem :: HEYTING1:25



     Th25: (( @ u) ^ {a}) = {} implies (( Atom A) . a) [= (( pseudo_compl A) . u)

    proof

      assume

       A1: (( @ u) ^ {a}) = {} ;

      now

        let c;

        assume c in (( Atom A) . a);

        then c = a by Th6;

        then

        consider b such that

         A2: b in ( - ( @ u)) and

         A3: b c= c by A1, Th19;

        consider d such that

         A4: d c= b and

         A5: d in ( mi ( - ( @ u))) by A2, NORMFORM: 41;

        take e = d;

        thus e in (( pseudo_compl A) . u) by A5, Def8;

        thus e c= c by A3, A4, NORMFORM: 2;

      end;

      hence thesis by Lm3;

    end;

    theorem :: HEYTING1:26



     Th26: (for b st b in u holds (b \/ a) in ( DISJOINT_PAIRS A)) & (u "/\" (( Atom A) . a)) [= w implies (( Atom A) . a) [= (( StrongImpl A) . (u,w))

    proof

      assume that

       A1: for b st b in u holds (b \/ a) in ( DISJOINT_PAIRS A) and

       A2: (u "/\" (( Atom A) . a)) [= w;

       A3:

      now

        let c;

        assume

         A4: c in u;

        then

         A5: (c \/ a) is Element of ( DISJOINT_PAIRS A) by A1;

        a in ( @ (( Atom A) . a)) by Th7;

        then (c \/ a) in (( @ u) ^ ( @ (( Atom A) . a))) by A1, A4, NORMFORM: 35;

        then

        consider b such that

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

         A7: b in ( mi (( @ u) ^ ( @ (( Atom A) . a)))) by A5, NORMFORM: 41;

        b in ( M(A) . (u,(( Atom A) . a))) by A7, NORMFORM:def 12;

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

        then

        consider d such that

         A8: d in w and

         A9: d c= b by A2, Lm2;

        take e = d;

        thus e in w by A8;

        thus e c= (c \/ a) by A6, A9, NORMFORM: 2;

      end;

      now

        let c;

        assume c in (( Atom A) . a);

        then c = a by Th6;

        then

        consider b such that

         A10: b in (( @ u) =>> ( @ w)) and

         A11: b c= c by A3, Th20;

        consider d such that

         A12: d c= b and

         A13: d in ( mi (( @ u) =>> ( @ w))) by A10, NORMFORM: 41;

        take e = d;

        thus e in (( StrongImpl A) . (u,w)) by A13, Def9;

        thus e c= c by A11, A12, NORMFORM: 2;

      end;

      hence thesis by Lm3;

    end;

     Lm9:

    now

      let A, u, v;

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

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

       A1:

      now

        let w;

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



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

        .= (( Bottom ( NormForm A)) "/\" si) by Th23

        .= ( Bottom ( NormForm A));

        assume w in ( SUB u);

        then

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

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

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

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

        .= (u "/\" (pc "/\" ((( StrongImpl A) [:] (( 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(A) [;] (u,Psi)) . w) [= (u2 "/\" si) by LATTICES: 6;

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

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

      end;

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

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

      let w;

      assume

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



       A6: v = ( FinJoin (( @ v),( Atom A))) by Th10;

      then

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

      now

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

        let a;

        assume a in ( @ v);

        then (( M(A) [;] (u,( Atom A))) . a) [= w by A7, A5, LATTICE2: 31;

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

        then

         A8: (u "/\" (( Atom A) . a)) [= w by LATTICES:def 2;

        consider v such that

         A9: v in ( SUB u) and

         A10: (( @ v) ^ {a}) = {} and

         A11: for b st b in (( diff u) . v) holds (b \/ a) in ( DISJOINT_PAIRS A) by Lm8;

        ((( diff u) . v) "/\" (( Atom A) . a)) [= (u "/\" (( Atom A) . a)) by Th22, LATTICES: 9;

        then ((( diff u) . v) "/\" (( Atom A) . a)) [= w by A8, LATTICES: 7;

        then (( Atom A) . a) [= (( StrongImpl A) . ((( diff u) . v),w)) by A11, Th26;

        then

         A12: (( Atom A) . a) [= (sf . v) by FUNCOP_1: 48;



         A13: ((pf . v) "/\" (sf . v)) = ( M(A) . ((pf . v),(sf . v))) by LATTICES:def 2

        .= (( M(A) .: (pf,sf)) . v) by FUNCOP_1: 37;

        (( Atom A) . a) [= (pf . v) by A10, Th25;

        then (( Atom A) . a) [= (( M(A) .: (pf,sf)) . v) by A12, A13, FILTER_0: 7;

        hence (( Atom A) . a) [= IMPL(u,w) by A9, LATTICE2: 29;

      end;

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

    end;



     Lm10: ( NormForm A) is implicative

    proof

      let p,q be Element of ( NormForm A);

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

      thus (p "/\" r) [= q & for r1 be Element of ( NormForm A) st (p "/\" r1) [= q holds r1 [= r by Lm9;

    end;

    registration

      let A;

      cluster ( NormForm A) -> implicative;

      coherence by Lm10;

    end

    theorem :: HEYTING1:27



     Th27: (u => v) = ( FinJoin (( SUB u),(the L_meet of ( NormForm A) .: (( pseudo_compl A),(( StrongImpl A) [:] (( diff u),v))))))

    proof

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

      (u "/\" IMPL(u,v)) [= v & for w st (u "/\" w) [= v holds w [= IMPL(u,v) by Lm9;

      hence thesis by FILTER_0:def 7;

    end;

    theorem :: HEYTING1:28

    ( Top ( NormForm A)) = { [ {} , {} ]}

    proof

      reconsider O = { [ {} , {} ]} as Element of ( Normal_forms_on A) by Th17;

      set sd = (( StrongImpl A) [:] (( diff ( Bottom ( NormForm A))),( Bottom ( NormForm A))));

      set F = ( M(A) .: (( pseudo_compl A),sd));



       A1: ( @ (( pseudo_compl A) . ( Bottom ( NormForm A)))) = ( mi ( - ( @ ( Bottom ( NormForm A))))) by Def8

      .= ( mi O) by Th13, NORMFORM: 57

      .= O by NORMFORM: 42;



       A2: ( Bottom ( NormForm A)) = {} by NORMFORM: 57;



      then (( diff ( Bottom ( NormForm A))) . ( Bottom ( NormForm A))) = ( {} \ {} ) by Def11

      .= ( Bottom ( NormForm A)) by NORMFORM: 57;



      then

       A3: ( @ (sd . ( Bottom ( NormForm A)))) = (( StrongImpl A) . (( Bottom ( NormForm A)),( Bottom ( NormForm A)))) by FUNCOP_1: 48

      .= ( mi (( @ ( Bottom ( NormForm A))) =>> ( @ ( Bottom ( NormForm A))))) by Def9

      .= ( mi O) by A2, Th14

      .= O by NORMFORM: 42;



      thus ( Top ( NormForm A)) = (( Bottom ( NormForm A)) => ( Bottom ( NormForm A))) by FILTER_0: 28

      .= ( FinJoin (( SUB ( Bottom ( NormForm A))),F)) by Th27

      .= ( J(A) $$ (( SUB ( Bottom ( NormForm A))),F)) by LATTICE2:def 3

      .= (F . ( Bottom ( NormForm A))) by A2, SETWISEO: 17, ZFMISC_1: 1

      .= ( M(A) . ((( pseudo_compl A) . ( Bottom ( NormForm A))),(sd . ( Bottom ( NormForm A))))) by FUNCOP_1: 37

      .= ( mi (O ^ O)) by A1, A3, NORMFORM:def 12

      .= { [ {} , {} ]} by Th3;

    end;