lukasi_1.miz

    begin

    reserve A for QC-alphabet;

    reserve p,q,r,s,t for Element of ( CQC-WFF A);

    reserve X for Subset of ( CQC-WFF A);

    theorem :: LUKASI_1:1



     Th1: ((p => q) => ((q => r) => (p => r))) in ( TAUT A)

    proof

      ((p => q) => (( 'not' (q '&' ( 'not' r))) => ( 'not' (p '&' ( 'not' r))))) in ( TAUT A) by CQC_THE1: 44;

      then ((p => q) => ((q => r) => ( 'not' (p '&' ( 'not' r))))) in ( TAUT A) by QC_LANG2:def 2;

      hence thesis by QC_LANG2:def 2;

    end;

    theorem :: LUKASI_1:2



     Th2: (p => q) in ( TAUT A) implies ((q => r) => (p => r)) in ( TAUT A)

    proof

      assume

       A1: (p => q) in ( TAUT A);

      ((p => q) => ((q => r) => (p => r))) in ( TAUT A) by Th1;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:3



     Th3: (p => q) in ( TAUT A) & (q => r) in ( TAUT A) implies (p => r) in ( TAUT A)

    proof

      assume that

       A1: (p => q) in ( TAUT A) and

       A2: (q => r) in ( TAUT A);

      ((p => q) => ((q => r) => (p => r))) in ( TAUT A) by Th1;

      then ((q => r) => (p => r)) in ( TAUT A) by A1, CQC_THE1: 46;

      hence thesis by A2, CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:4



     Th4: (p => p) in ( TAUT A)

    proof

      ((( 'not' p) => p) => p) in ( TAUT A) & (p => (( 'not' p) => p)) in ( TAUT A) by CQC_THE1: 42, CQC_THE1: 43;

      hence thesis by Th3;

    end;



     Lm1: ((((q => r) => (p => r)) => s) => ((p => q) => s)) in ( TAUT A)

    proof

      ((p => q) => ((q => r) => (p => r))) in ( TAUT A) by Th1;

      hence thesis by Th2;

    end;



     Lm2: ((p => (q => r)) => ((s => q) => (p => (s => r)))) in ( TAUT A)

    proof

      (((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r)))) => ((p => (q => r)) => ((s => q) => (p => (s => r))))) in ( TAUT A) & ((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r)))) in ( TAUT A) by Lm1;

      hence thesis by CQC_THE1: 46;

    end;



     Lm3: ((p => q) => (((p => r) => s) => ((q => r) => s))) in ( TAUT A)

    proof

      (((q => r) => (p => r)) => (((p => r) => s) => ((q => r) => s))) in ( TAUT A) & ((((q => r) => (p => r)) => (((p => r) => s) => ((q => r) => s))) => ((p => q) => (((p => r) => s) => ((q => r) => s)))) in ( TAUT A) by Lm1, Th1;

      hence thesis by CQC_THE1: 46;

    end;



     Lm4: ((t => ((p => r) => s)) => ((p => q) => (t => ((q => r) => s)))) in ( TAUT A)

    proof

      ((p => q) => (((p => r) => s) => ((q => r) => s))) in ( TAUT A) & (((p => q) => (((p => r) => s) => ((q => r) => s))) => ((t => ((p => r) => s)) => ((p => q) => (t => ((q => r) => s))))) in ( TAUT A) by Lm2, Lm3;

      hence thesis by CQC_THE1: 46;

    end;



     Lm5: (((( 'not' p) => q) => r) => (p => r)) in ( TAUT A)

    proof

      (p => (( 'not' p) => q)) in ( TAUT A) by CQC_THE1: 43;

      hence thesis by Th2;

    end;



     Lm6: (p => (((( 'not' p) => r) => s) => ((q => r) => s))) in ( TAUT A)

    proof

      ((( 'not' p) => q) => (((( 'not' p) => r) => s) => ((q => r) => s))) in ( TAUT A) & (((( 'not' p) => q) => (((( 'not' p) => r) => s) => ((q => r) => s))) => (p => (((( 'not' p) => r) => s) => ((q => r) => s)))) in ( TAUT A) by Lm3, Lm5;

      hence thesis by CQC_THE1: 46;

    end;



     Lm7: ((q => ((( 'not' p) => p) => p)) => ((( 'not' p) => p) => p)) in ( TAUT A)

    proof

      ((( 'not' p) => p) => p) in ( TAUT A) & (((( 'not' p) => p) => p) => (((( 'not' ((( 'not' p) => p) => p)) => ((( 'not' p) => p) => p)) => ((( 'not' p) => p) => p)) => ((q => ((( 'not' p) => p) => p)) => ((( 'not' p) => p) => p)))) in ( TAUT A) by Lm6, CQC_THE1: 42;

      then ((( 'not' ((( 'not' p) => p) => p)) => ((( 'not' p) => p) => p)) => ((( 'not' p) => p) => p)) in ( TAUT A) & (((( 'not' ((( 'not' p) => p) => p)) => ((( 'not' p) => p) => p)) => ((( 'not' p) => p) => p)) => ((q => ((( 'not' p) => p) => p)) => ((( 'not' p) => p) => p))) in ( TAUT A) by CQC_THE1: 42, CQC_THE1: 46;

      hence thesis by CQC_THE1: 46;

    end;



     Lm8: (t => ((( 'not' p) => p) => p)) in ( TAUT A)

    proof

      ((( 'not' t) => ((( 'not' p) => p) => p)) => ((( 'not' p) => p) => p)) in ( TAUT A) & (((( 'not' t) => ((( 'not' p) => p) => p)) => ((( 'not' p) => p) => p)) => (t => ((( 'not' p) => p) => p))) in ( TAUT A) by Lm5, Lm7;

      hence thesis by CQC_THE1: 46;

    end;



     Lm9: ((( 'not' p) => q) => (t => ((q => p) => p))) in ( TAUT A)

    proof

      (t => ((( 'not' p) => p) => p)) in ( TAUT A) & ((t => ((( 'not' p) => p) => p)) => ((( 'not' p) => q) => (t => ((q => p) => p)))) in ( TAUT A) by Lm4, Lm8;

      hence thesis by CQC_THE1: 46;

    end;



     Lm10: (((t => ((q => p) => p)) => r) => ((( 'not' p) => q) => r)) in ( TAUT A)

    proof

      ((( 'not' p) => q) => (t => ((q => p) => p))) in ( TAUT A) & (((( 'not' p) => q) => (t => ((q => p) => p))) => (((t => ((q => p) => p)) => r) => ((( 'not' p) => q) => r))) in ( TAUT A) by Lm9, Th1;

      hence thesis by CQC_THE1: 46;

    end;



     Lm11: ((( 'not' p) => q) => ((q => p) => p)) in ( TAUT A)

    proof

      ((( 'not' ((q => p) => p)) => ((q => p) => p)) => ((q => p) => p)) in ( TAUT A) & (((( 'not' ((q => p) => p)) => ((q => p) => p)) => ((q => p) => p)) => ((( 'not' p) => q) => ((q => p) => p))) in ( TAUT A) by Lm10, CQC_THE1: 42;

      hence thesis by CQC_THE1: 46;

    end;



     Lm12: (p => ((q => p) => p)) in ( TAUT A)

    proof

      ((( 'not' p) => q) => ((q => p) => p)) in ( TAUT A) & (((( 'not' p) => q) => ((q => p) => p)) => (p => ((q => p) => p))) in ( TAUT A) by Lm5, Lm11;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:5



     Th5: (q => (p => q)) in ( TAUT A)

    proof

      (q => ((( 'not' p) => q) => q)) in ( TAUT A) & ((q => ((( 'not' p) => q) => q)) => ((p => (( 'not' p) => q)) => (q => (p => q)))) in ( TAUT A) by Lm2, Lm12;

      then (p => (( 'not' p) => q)) in ( TAUT A) & ((p => (( 'not' p) => q)) => (q => (p => q))) in ( TAUT A) by CQC_THE1: 43, CQC_THE1: 46;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:6



     Th6: (((p => q) => r) => (q => r)) in ( TAUT A)

    proof

      (q => (p => q)) in ( TAUT A) & ((q => (p => q)) => (((p => q) => r) => (q => r))) in ( TAUT A) by Th1, Th5;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:7



     Th7: (q => ((q => p) => p)) in ( TAUT A)

    proof

      ((( 'not' p) => q) => ((q => p) => p)) in ( TAUT A) & (((( 'not' p) => q) => ((q => p) => p)) => (q => ((q => p) => p))) in ( TAUT A) by Lm11, Th6;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:8



     Th8: ((s => (q => p)) => (q => (s => p))) in ( TAUT A)

    proof

      (q => ((q => p) => p)) in ( TAUT A) & ((q => ((q => p) => p)) => ((s => (q => p)) => (q => (s => p)))) in ( TAUT A) by Lm2, Th7;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:9



     Th9: ((q => r) => ((p => q) => (p => r))) in ( TAUT A)

    proof

      ((p => q) => ((q => r) => (p => r))) in ( TAUT A) & (((p => q) => ((q => r) => (p => r))) => ((q => r) => ((p => q) => (p => r)))) in ( TAUT A) by Th1, Th8;

      hence thesis by CQC_THE1: 46;

    end;



     Lm13: (((q => (s => p)) => r) => ((s => (q => p)) => r)) in ( TAUT A)

    proof

      ((s => (q => p)) => (q => (s => p))) in ( TAUT A) & (((s => (q => p)) => (q => (s => p))) => (((q => (s => p)) => r) => ((s => (q => p)) => r))) in ( TAUT A) by Th1, Th8;

      hence thesis by CQC_THE1: 46;

    end;



     Lm14: (((p => q) => p) => p) in ( TAUT A)

    proof

      ((( 'not' p) => (p => q)) => (((p => q) => p) => p)) in ( TAUT A) & (((( 'not' p) => (p => q)) => (((p => q) => p) => p)) => ((p => (( 'not' p) => q)) => (((p => q) => p) => p))) in ( TAUT A) by Lm11, Lm13;

      then (p => (( 'not' p) => q)) in ( TAUT A) & ((p => (( 'not' p) => q)) => (((p => q) => p) => p)) in ( TAUT A) by CQC_THE1: 43, CQC_THE1: 46;

      hence thesis by CQC_THE1: 46;

    end;



     Lm15: (((p => r) => s) => ((p => q) => ((q => r) => s))) in ( TAUT A)

    proof

      ((p => q) => (((p => r) => s) => ((q => r) => s))) in ( TAUT A) & (((p => q) => (((p => r) => s) => ((q => r) => s))) => (((p => r) => s) => ((p => q) => ((q => r) => s)))) in ( TAUT A) by Lm3, Th8;

      hence thesis by CQC_THE1: 46;

    end;



     Lm16: (((p => q) => r) => ((r => p) => p)) in ( TAUT A)

    proof

      (((p => q) => p) => p) in ( TAUT A) & ((((p => q) => p) => p) => (((p => q) => r) => ((r => p) => p))) in ( TAUT A) by Lm14, Lm15;

      hence thesis by CQC_THE1: 46;

    end;



     Lm17: ((((r => p) => p) => s) => (((p => q) => r) => s)) in ( TAUT A)

    proof

      (((p => q) => r) => ((r => p) => p)) in ( TAUT A) & ((((p => q) => r) => ((r => p) => p)) => ((((r => p) => p) => s) => (((p => q) => r) => s))) in ( TAUT A) by Lm16, Th1;

      hence thesis by CQC_THE1: 46;

    end;



     Lm18: (((q => r) => p) => ((q => p) => p)) in ( TAUT A)

    proof

      (((p => q) => q) => ((q => p) => p)) in ( TAUT A) & ((((p => q) => q) => ((q => p) => p)) => (((q => r) => p) => ((q => p) => p))) in ( TAUT A) by Lm16, Lm17;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:10



     Th10: ((q => (q => r)) => (q => r)) in ( TAUT A)

    proof

      ((q => r) => (q => r)) in ( TAUT A) & (((q => r) => (q => r)) => ((q => (q => r)) => (q => r))) in ( TAUT A) by Lm18, Th4;

      hence thesis by CQC_THE1: 46;

    end;



     Lm19: ((q => s) => (((q => r) => p) => ((s => p) => p))) in ( TAUT A)

    proof

      (((q => r) => p) => ((q => p) => p)) in ( TAUT A) & ((((q => r) => p) => ((q => p) => p)) => ((q => s) => (((q => r) => p) => ((s => p) => p)))) in ( TAUT A) by Lm4, Lm18;

      hence thesis by CQC_THE1: 46;

    end;



     Lm20: (((q => r) => p) => ((q => s) => ((s => p) => p))) in ( TAUT A)

    proof

      ((q => s) => (((q => r) => p) => ((s => p) => p))) in ( TAUT A) & (((q => s) => (((q => r) => p) => ((s => p) => p))) => (((q => r) => p) => ((q => s) => ((s => p) => p)))) in ( TAUT A) by Lm19, Th8;

      hence thesis by CQC_THE1: 46;

    end;



     Lm21: ((q => s) => ((s => (p => (q => r))) => (p => (q => r)))) in ( TAUT A)

    proof

      ((q => r) => (p => (q => r))) in ( TAUT A) & (((q => r) => (p => (q => r))) => ((q => s) => ((s => (p => (q => r))) => (p => (q => r))))) in ( TAUT A) by Lm20, Th5;

      hence thesis by CQC_THE1: 46;

    end;



     Lm22: ((s => (p => (q => r))) => ((q => s) => (p => (q => r)))) in ( TAUT A)

    proof

      ((q => s) => ((s => (p => (q => r))) => (p => (q => r)))) in ( TAUT A) & (((q => s) => ((s => (p => (q => r))) => (p => (q => r)))) => ((s => (p => (q => r))) => ((q => s) => (p => (q => r))))) in ( TAUT A) by Lm21, Th8;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:11



     Th11: ((p => (q => r)) => ((p => q) => (p => r))) in ( TAUT A)

    proof

      ((q => r) => ((p => q) => (p => r))) in ( TAUT A) & (((q => r) => ((p => q) => (p => r))) => ((p => (q => r)) => ((p => q) => (p => r)))) in ( TAUT A) by Lm22, Th9;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:12



     Th12: (( 'not' ( VERUM A)) => p) in ( TAUT A)

    proof

      (( VERUM A) => (( 'not' ( VERUM A)) => p)) in ( TAUT A) by CQC_THE1: 43;

      hence thesis by CQC_THE1: 41, CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:13



     Th13: q in ( TAUT A) implies (p => q) in ( TAUT A)

    proof

      (q => (p => q)) in ( TAUT A) by Th5;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:14

    p in ( TAUT A) implies ((p => q) => q) in ( TAUT A)

    proof

      assume

       A1: p in ( TAUT A);

      (p => ((p => q) => q)) in ( TAUT A) by Th7;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:15



     Th15: (s => (q => p)) in ( TAUT A) implies (q => (s => p)) in ( TAUT A)

    proof

      assume

       A1: (s => (q => p)) in ( TAUT A);

      ((s => (q => p)) => (q => (s => p))) in ( TAUT A) by Th8;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:16



     Th16: (s => (q => p)) in ( TAUT A) & q in ( TAUT A) implies (s => p) in ( TAUT A)

    proof

      assume (s => (q => p)) in ( TAUT A);

      then (q => (s => p)) in ( TAUT A) by Th15;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:17

    (s => (q => p)) in ( TAUT A) & q in ( TAUT A) & s in ( TAUT A) implies p in ( TAUT A)

    proof

      assume (s => (q => p)) in ( TAUT A) & q in ( TAUT A);

      then (s => p) in ( TAUT A) by Th16;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:18

    (q => (q => r)) in ( TAUT A) implies (q => r) in ( TAUT A)

    proof

      ((q => (q => r)) => (q => r)) in ( TAUT A) by Th10;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:19



     Th19: (p => (q => r)) in ( TAUT A) implies ((p => q) => (p => r)) in ( TAUT A)

    proof

      assume

       A1: (p => (q => r)) in ( TAUT A);

      ((p => (q => r)) => ((p => q) => (p => r))) in ( TAUT A) by Th11;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:20



     Th20: (p => (q => r)) in ( TAUT A) & (p => q) in ( TAUT A) implies (p => r) in ( TAUT A)

    proof

      assume (p => (q => r)) in ( TAUT A);

      then ((p => q) => (p => r)) in ( TAUT A) by Th19;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:21

    (p => (q => r)) in ( TAUT A) & (p => q) in ( TAUT A) & p in ( TAUT A) implies r in ( TAUT A)

    proof

      assume (p => (q => r)) in ( TAUT A) & (p => q) in ( TAUT A);

      then (p => r) in ( TAUT A) by Th20;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:22



     Th22: (p => (q => r)) in ( TAUT A) & (p => (r => s)) in ( TAUT A) implies (p => (q => s)) in ( TAUT A)

    proof

      assume that

       A1: (p => (q => r)) in ( TAUT A) and

       A2: (p => (r => s)) in ( TAUT A);

      (p => ((q => r) => ((r => s) => (q => s)))) in ( TAUT A) by Th1, Th13;

      then (p => ((r => s) => (q => s))) in ( TAUT A) by A1, Th20;

      hence thesis by A2, Th20;

    end;

    theorem :: LUKASI_1:23

    (p => ( VERUM A)) in ( TAUT A) by Th13, CQC_THE1: 41;



     Lm23: (( 'not' p) => (p => ( 'not' ( VERUM A)))) in ( TAUT A)

    proof

      (p => (( 'not' p) => ( 'not' ( VERUM A)))) in ( TAUT A) by CQC_THE1: 43;

      hence thesis by Th15;

    end;



     Lm24: ((( 'not' p) => ( 'not' ( VERUM A))) => p) in ( TAUT A)

    proof

      (( 'not' p) => (( 'not' ( VERUM A)) => p)) in ( TAUT A) & ((( 'not' p) => (( 'not' ( VERUM A)) => p)) => ((( 'not' p) => ( 'not' ( VERUM A))) => (( 'not' p) => p))) in ( TAUT A) by Th11, Th12, Th13;

      then

       A1: ((( 'not' p) => ( 'not' ( VERUM A))) => (( 'not' p) => p)) in ( TAUT A) by CQC_THE1: 46;

      ((( 'not' p) => p) => p) in ( TAUT A) by CQC_THE1: 42;

      hence thesis by A1, Th3;

    end;

    theorem :: LUKASI_1:24



     Th24: ((( 'not' p) => ( 'not' q)) => (q => p)) in ( TAUT A)

    proof

      (q => (( 'not' q) => ( 'not' ( VERUM A)))) in ( TAUT A) & ((( 'not' q) => ( 'not' ( VERUM A))) => ((( 'not' p) => ( 'not' q)) => (( 'not' p) => ( 'not' ( VERUM A))))) in ( TAUT A) by Th9, CQC_THE1: 43;

      then

       A1: (q => ((( 'not' p) => ( 'not' q)) => (( 'not' p) => ( 'not' ( VERUM A))))) in ( TAUT A) by Th3;

      (q => ((( 'not' p) => ( 'not' ( VERUM A))) => p)) in ( TAUT A) by Lm24, Th13;

      then (q => ((( 'not' p) => ( 'not' q)) => p)) in ( TAUT A) by A1, Th22;

      hence thesis by Th15;

    end;

    theorem :: LUKASI_1:25



     Th25: (( 'not' ( 'not' p)) => p) in ( TAUT A)

    proof

      (( 'not' ( 'not' p)) => (( 'not' p) => ( 'not' ( VERUM A)))) in ( TAUT A) & ((( 'not' p) => ( 'not' ( VERUM A))) => (( VERUM A) => p)) in ( TAUT A) by Lm23, Th24;

      then (( 'not' ( 'not' p)) => (( VERUM A) => p)) in ( TAUT A) by Th3;

      then (( VERUM A) => (( 'not' ( 'not' p)) => p)) in ( TAUT A) by Th15;

      hence thesis by CQC_THE1: 41, CQC_THE1: 46;

    end;

     Lm25:

    now

      let A, p;

      (( 'not' ( 'not' p)) => p) in ( TAUT A) by Th25;

      then

       A1: ((p => ( 'not' ( VERUM A))) => (( 'not' ( 'not' p)) => ( 'not' ( VERUM A)))) in ( TAUT A) by Th2;

      ((( 'not' ( 'not' p)) => ( 'not' ( VERUM A))) => ( 'not' p)) in ( TAUT A) by Lm24;

      hence ((p => ( 'not' ( VERUM A))) => ( 'not' p)) in ( TAUT A) by A1, Th3;

    end;

    theorem :: LUKASI_1:26



     Th26: ((p => q) => (( 'not' q) => ( 'not' p))) in ( TAUT A)

    proof

      (( 'not' q) => (q => ( 'not' ( VERUM A)))) in ( TAUT A) & ((q => ( 'not' ( VERUM A))) => ((p => q) => (p => ( 'not' ( VERUM A))))) in ( TAUT A) by Lm23, Th9;

      then

       A1: (( 'not' q) => ((p => q) => (p => ( 'not' ( VERUM A))))) in ( TAUT A) by Th3;

      (( 'not' q) => ((p => ( 'not' ( VERUM A))) => ( 'not' p))) in ( TAUT A) by Lm25, Th13;

      then (( 'not' q) => ((p => q) => ( 'not' p))) in ( TAUT A) by A1, Th22;

      hence thesis by Th15;

    end;

    theorem :: LUKASI_1:27



     Th27: (p => ( 'not' ( 'not' p))) in ( TAUT A)

    proof

      ((( VERUM A) => p) => (( 'not' p) => ( 'not' ( VERUM A)))) in ( TAUT A) & ((( 'not' p) => ( 'not' ( VERUM A))) => ( 'not' ( 'not' p))) in ( TAUT A) by Lm25, Th26;

      then

       A1: ((( VERUM A) => p) => ( 'not' ( 'not' p))) in ( TAUT A) by Th3;

      (p => (( VERUM A) => p)) in ( TAUT A) by Th5;

      hence thesis by A1, Th3;

    end;

    theorem :: LUKASI_1:28



     Th28: ((( 'not' ( 'not' p)) => q) => (p => q)) in ( TAUT A) & ((p => q) => (( 'not' ( 'not' p)) => q)) in ( TAUT A)

    proof

      (p => ( 'not' ( 'not' p))) in ( TAUT A) by Th27;

      hence ((( 'not' ( 'not' p)) => q) => (p => q)) in ( TAUT A) by Th2;

      (( 'not' ( 'not' p)) => p) in ( TAUT A) by Th25;

      hence thesis by Th2;

    end;

    theorem :: LUKASI_1:29



     Th29: ((p => ( 'not' ( 'not' q))) => (p => q)) in ( TAUT A) & ((p => q) => (p => ( 'not' ( 'not' q)))) in ( TAUT A)

    proof

      ((p => (( 'not' ( 'not' q)) => q)) => ((p => ( 'not' ( 'not' q))) => (p => q))) in ( TAUT A) & (p => (( 'not' ( 'not' q)) => q)) in ( TAUT A) by Th11, Th13, Th25;

      hence ((p => ( 'not' ( 'not' q))) => (p => q)) in ( TAUT A) by CQC_THE1: 46;

      ((p => (q => ( 'not' ( 'not' q)))) => ((p => q) => (p => ( 'not' ( 'not' q))))) in ( TAUT A) & (p => (q => ( 'not' ( 'not' q)))) in ( TAUT A) by Th11, Th13, Th27;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:30



     Th30: ((p => ( 'not' q)) => (q => ( 'not' p))) in ( TAUT A)

    proof

      ((p => ( 'not' q)) => (( 'not' ( 'not' q)) => ( 'not' p))) in ( TAUT A) & ((( 'not' ( 'not' q)) => ( 'not' p)) => (q => ( 'not' p))) in ( TAUT A) by Th26, Th28;

      hence thesis by Th3;

    end;

    theorem :: LUKASI_1:31



     Th31: ((( 'not' p) => q) => (( 'not' q) => p)) in ( TAUT A)

    proof

      ((( 'not' p) => q) => (( 'not' q) => ( 'not' ( 'not' p)))) in ( TAUT A) & ((( 'not' q) => ( 'not' ( 'not' p))) => (( 'not' q) => p)) in ( TAUT A) by Th26, Th29;

      hence thesis by Th3;

    end;

    theorem :: LUKASI_1:32

    ((p => ( 'not' p)) => ( 'not' p)) in ( TAUT A)

    proof

      ((( 'not' ( 'not' p)) => ( 'not' p)) => ( 'not' p)) in ( TAUT A) & ((p => ( 'not' p)) => (( 'not' ( 'not' p)) => ( 'not' p))) in ( TAUT A) by Th28, CQC_THE1: 42;

      hence thesis by Th3;

    end;

    theorem :: LUKASI_1:33

    (( 'not' p) => (p => q)) in ( TAUT A)

    proof

      (( 'not' p) => (( 'not' ( 'not' p)) => q)) in ( TAUT A) & ((( 'not' ( 'not' p)) => q) => (p => q)) in ( TAUT A) by Th28, CQC_THE1: 43;

      hence thesis by Th3;

    end;

    theorem :: LUKASI_1:34



     Th34: (p => q) in ( TAUT A) iff (( 'not' q) => ( 'not' p)) in ( TAUT A)

    proof

      ((p => q) => (( 'not' q) => ( 'not' p))) in ( TAUT A) by Th26;

      hence (p => q) in ( TAUT A) implies (( 'not' q) => ( 'not' p)) in ( TAUT A) by CQC_THE1: 46;

      ((( 'not' q) => ( 'not' p)) => (p => q)) in ( TAUT A) by Th24;

      hence (( 'not' q) => ( 'not' p)) in ( TAUT A) implies (p => q) in ( TAUT A) by CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:35

    (( 'not' p) => ( 'not' q)) in ( TAUT A) implies (q => p) in ( TAUT A) by Th34;

    theorem :: LUKASI_1:36

    p in ( TAUT A) iff ( 'not' ( 'not' p)) in ( TAUT A)

    proof

      thus p in ( TAUT A) implies ( 'not' ( 'not' p)) in ( TAUT A)

      proof

        assume

         A1: p in ( TAUT A);

        (p => ( 'not' ( 'not' p))) in ( TAUT A) by Th27;

        hence thesis by A1, CQC_THE1: 46;

      end;

      assume

       A2: ( 'not' ( 'not' p)) in ( TAUT A);

      (( 'not' ( 'not' p)) => p) in ( TAUT A) by Th25;

      hence thesis by A2, CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:37

    (p => q) in ( TAUT A) iff (p => ( 'not' ( 'not' q))) in ( TAUT A)

    proof

      thus (p => q) in ( TAUT A) implies (p => ( 'not' ( 'not' q))) in ( TAUT A)

      proof

        assume

         A1: (p => q) in ( TAUT A);

        ((p => q) => (p => ( 'not' ( 'not' q)))) in ( TAUT A) by Th29;

        hence thesis by A1, CQC_THE1: 46;

      end;

      assume

       A2: (p => ( 'not' ( 'not' q))) in ( TAUT A);

      ((p => ( 'not' ( 'not' q))) => (p => q)) in ( TAUT A) by Th29;

      hence thesis by A2, CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:38

    (p => q) in ( TAUT A) iff (( 'not' ( 'not' p)) => q) in ( TAUT A)

    proof

      thus (p => q) in ( TAUT A) implies (( 'not' ( 'not' p)) => q) in ( TAUT A)

      proof

        assume

         A1: (p => q) in ( TAUT A);

        ((p => q) => (( 'not' ( 'not' p)) => q)) in ( TAUT A) by Th28;

        hence thesis by A1, CQC_THE1: 46;

      end;

      assume

       A2: (( 'not' ( 'not' p)) => q) in ( TAUT A);

      ((( 'not' ( 'not' p)) => q) => (p => q)) in ( TAUT A) by Th28;

      hence thesis by A2, CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:39

    (p => ( 'not' q)) in ( TAUT A) implies (q => ( 'not' p)) in ( TAUT A)

    proof

      assume

       A1: (p => ( 'not' q)) in ( TAUT A);

      ((p => ( 'not' q)) => (q => ( 'not' p))) in ( TAUT A) by Th30;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: LUKASI_1:40

    (( 'not' p) => q) in ( TAUT A) implies (( 'not' q) => p) in ( TAUT A)

    proof

      assume

       A1: (( 'not' p) => q) in ( TAUT A);

      ((( 'not' p) => q) => (( 'not' q) => p)) in ( TAUT A) by Th31;

      hence thesis by A1, CQC_THE1: 46;

    end;

    registration

      let A, p, q, r;

      cluster ((p => q) => ((q => r) => (p => r))) -> valid;

      coherence by Th1;

    end

    theorem :: LUKASI_1:41

    (p => q) is valid implies ((q => r) => (p => r)) is valid

    proof

      assume

       A1: (p => q) is valid;

      ((p => q) => ((q => r) => (p => r))) is valid;

      hence thesis by A1, CQC_THE1: 65;

    end;

    theorem :: LUKASI_1:42



     Th42: (p => q) is valid & (q => r) is valid implies (p => r) is valid by Th3;

    registration

      let A, p;

      cluster (p => p) -> valid;

      coherence by Th4;

    end

    registration

      let A, p, q;

      cluster (p => (q => p)) -> valid;

      coherence by Th5;

    end

    theorem :: LUKASI_1:43

    p is valid implies (q => p) is valid by Th13;

    registration

      let A, p, q, s;

      cluster ((s => (q => p)) => (q => (s => p))) -> valid;

      coherence by Th8;

    end

    theorem :: LUKASI_1:44



     Th44: (p => (q => r)) is valid implies (q => (p => r)) is valid by Th15;

    theorem :: LUKASI_1:45

    (p => (q => r)) is valid & q is valid implies (p => r) is valid

    proof

      assume (p => (q => r)) is valid;

      then (q => (p => r)) is valid by Th44;

      hence thesis by CQC_THE1: 65;

    end;

    theorem :: LUKASI_1:46

    (p => ( VERUM A)) is valid & (( 'not' ( VERUM A)) => p) is valid by Th13, CQC_THE1: 41, Th12;

    registration

      let A, p, q;

      cluster (p => ((p => q) => q)) -> valid;

      coherence by Th7;

    end

    registration

      let A, q, r;

      cluster ((q => (q => r)) => (q => r)) -> valid;

      coherence by Th10;

    end

    theorem :: LUKASI_1:47

    (q => (q => r)) is valid implies (q => r) is valid

    proof

      assume

       A1: (q => (q => r)) is valid;

      ((q => (q => r)) => (q => r)) is valid;

      hence thesis by A1, CQC_THE1: 65;

    end;

    registration

      let A, p, q, r;

      cluster ((p => (q => r)) => ((p => q) => (p => r))) -> valid;

      coherence by Th11;

    end

    theorem :: LUKASI_1:48



     Th48: (p => (q => r)) is valid implies ((p => q) => (p => r)) is valid

    proof

      assume

       A1: (p => (q => r)) is valid;

      ((p => (q => r)) => ((p => q) => (p => r))) is valid;

      hence thesis by A1, CQC_THE1: 65;

    end;

    theorem :: LUKASI_1:49

    (p => (q => r)) is valid & (p => q) is valid implies (p => r) is valid

    proof

      assume that

       A1: (p => (q => r)) is valid and

       A2: (p => q) is valid;

      ((p => q) => (p => r)) is valid by A1, Th48;

      hence thesis by A2, CQC_THE1: 65;

    end;

    registration

      let A, p, q, r;

      cluster (((p => q) => r) => (q => r)) -> valid;

      coherence by Th6;

    end

    theorem :: LUKASI_1:50

    ((p => q) => r) is valid implies (q => r) is valid

    proof

      assume

       A1: ((p => q) => r) is valid;

      (((p => q) => r) => (q => r)) is valid;

      hence thesis by A1, CQC_THE1: 65;

    end;

    registration

      let A, p, q, r;

      cluster ((p => q) => ((r => p) => (r => q))) -> valid;

      coherence by Th9;

    end

    theorem :: LUKASI_1:51

    (p => q) is valid implies ((r => p) => (r => q)) is valid

    proof

      assume

       A1: (p => q) is valid;

      ((p => q) => ((r => p) => (r => q))) is valid;

      hence thesis by A1, CQC_THE1: 65;

    end;

    registration

      let A, p, q;

      cluster ((p => q) => (( 'not' q) => ( 'not' p))) -> valid;

      coherence by Th26;

    end

    registration

      let A, p, q;

      cluster ((( 'not' p) => ( 'not' q)) => (q => p)) -> valid;

      coherence by Th24;

    end

    theorem :: LUKASI_1:52

    (( 'not' p) => ( 'not' q)) is valid iff (q => p) is valid

    proof

      thus (( 'not' p) => ( 'not' q)) is valid implies (q => p) is valid

      proof

        assume

         A1: (( 'not' p) => ( 'not' q)) is valid;

        ((( 'not' p) => ( 'not' q)) => (q => p)) is valid;

        hence thesis by A1, CQC_THE1: 65;

      end;

      assume

       A2: (q => p) is valid;

      ((q => p) => (( 'not' p) => ( 'not' q))) is valid;

      hence thesis by A2, CQC_THE1: 65;

    end;

    registration

      let A, p;

      cluster (p => ( 'not' ( 'not' p))) -> valid;

      coherence by Th27;

    end

    registration

      let A, p;

      cluster (( 'not' ( 'not' p)) => p) -> valid;

      coherence by Th25;

    end

    theorem :: LUKASI_1:53

    ( 'not' ( 'not' p)) is valid iff p is valid

    proof

      thus ( 'not' ( 'not' p)) is valid implies p is valid

      proof

        assume

         A1: ( 'not' ( 'not' p)) is valid;

        (( 'not' ( 'not' p)) => p) is valid;

        hence thesis by A1, CQC_THE1: 65;

      end;

      assume

       A2: p is valid;

      (p => ( 'not' ( 'not' p))) is valid;

      hence thesis by A2, CQC_THE1: 65;

    end;

    registration

      let A, p, q;

      cluster ((( 'not' ( 'not' p)) => q) => (p => q)) -> valid;

      coherence by Th28;

    end

    theorem :: LUKASI_1:54

    (( 'not' ( 'not' p)) => q) is valid iff (p => q) is valid

    proof

      thus (( 'not' ( 'not' p)) => q) is valid implies (p => q) is valid

      proof

        assume

         A1: (( 'not' ( 'not' p)) => q) is valid;

        ((( 'not' ( 'not' p)) => q) => (p => q)) is valid;

        hence thesis by A1, CQC_THE1: 65;

      end;

      assume

       A2: (p => q) is valid;

      (( 'not' ( 'not' p)) => p) is valid;

      hence thesis by A2, Th42;

    end;

    registration

      let A, p, q;

      cluster ((p => ( 'not' ( 'not' q))) => (p => q)) -> valid;

      coherence by Th29;

    end

    theorem :: LUKASI_1:55

    (p => ( 'not' ( 'not' q))) is valid iff (p => q) is valid

    proof

      thus (p => ( 'not' ( 'not' q))) is valid implies (p => q) is valid

      proof

        assume

         A1: (p => ( 'not' ( 'not' q))) is valid;

        ((p => ( 'not' ( 'not' q))) => (p => q)) is valid;

        hence thesis by A1, CQC_THE1: 65;

      end;

      assume

       A2: (p => q) is valid;

      (q => ( 'not' ( 'not' q))) is valid;

      hence thesis by A2, Th42;

    end;

    registration

      let A, p, q;

      cluster ((p => ( 'not' q)) => (q => ( 'not' p))) -> valid;

      coherence by Th30;

    end

    theorem :: LUKASI_1:56

    (p => ( 'not' q)) is valid implies (q => ( 'not' p)) is valid

    proof

      assume

       A1: (p => ( 'not' q)) is valid;

      ((p => ( 'not' q)) => (q => ( 'not' p))) is valid;

      hence thesis by A1, CQC_THE1: 65;

    end;

    registration

      let A, p, q;

      cluster ((( 'not' p) => q) => (( 'not' q) => p)) -> valid;

      coherence by Th31;

    end

    theorem :: LUKASI_1:57

    (( 'not' p) => q) is valid implies (( 'not' q) => p) is valid

    proof

      assume

       A1: (( 'not' p) => q) is valid;

      ((( 'not' p) => q) => (( 'not' q) => p)) is valid;

      hence thesis by A1, CQC_THE1: 65;

    end;

    theorem :: LUKASI_1:58

    X |- (p => q) implies X |- ((q => r) => (p => r))

    proof

      assume

       A1: X |- (p => q);

      X |- ((p => q) => ((q => r) => (p => r))) by CQC_THE1: 59;

      hence thesis by A1, CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:59



     Th59: X |- (p => q) & X |- (q => r) implies X |- (p => r)

    proof

      assume that

       A1: X |- (p => q) and

       A2: X |- (q => r);

      X |- ((p => q) => ((q => r) => (p => r))) by CQC_THE1: 59;

      then X |- ((q => r) => (p => r)) by A1, CQC_THE1: 55;

      hence thesis by A2, CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:60

    X |- (p => p) by CQC_THE1: 59;

    theorem :: LUKASI_1:61

    X |- p implies X |- (q => p)

    proof

      assume

       A1: X |- p;

      X |- (p => (q => p)) by CQC_THE1: 59;

      hence thesis by A1, CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:62

    X |- p implies X |- ((p => q) => q)

    proof

      assume

       A1: X |- p;

      X |- (p => ((p => q) => q)) by CQC_THE1: 59;

      hence thesis by A1, CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:63



     Th63: X |- (p => (q => r)) implies X |- (q => (p => r))

    proof

      assume

       A1: X |- (p => (q => r));

      X |- ((p => (q => r)) => (q => (p => r))) by CQC_THE1: 59;

      hence thesis by A1, CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:64

    X |- (p => (q => r)) & X |- q implies X |- (p => r)

    proof

      assume X |- (p => (q => r));

      then X |- (q => (p => r)) by Th63;

      hence thesis by CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:65

    X |- (p => (p => q)) implies X |- (p => q)

    proof

      assume

       A1: X |- (p => (p => q));

      X |- ((p => (p => q)) => (p => q)) by CQC_THE1: 59;

      hence thesis by A1, CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:66

    X |- ((p => q) => r) implies X |- (q => r)

    proof

      assume

       A1: X |- ((p => q) => r);

      X |- (((p => q) => r) => (q => r)) by CQC_THE1: 59;

      hence thesis by A1, CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:67



     Th67: X |- (p => (q => r)) implies X |- ((p => q) => (p => r))

    proof

      assume

       A1: X |- (p => (q => r));

      X |- ((p => (q => r)) => ((p => q) => (p => r))) by CQC_THE1: 59;

      hence thesis by A1, CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:68

    X |- (p => (q => r)) & X |- (p => q) implies X |- (p => r)

    proof

      assume X |- (p => (q => r));

      then X |- ((p => q) => (p => r)) by Th67;

      hence thesis by CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:69

    X |- (( 'not' p) => ( 'not' q)) iff X |- (q => p)

    proof

      thus X |- (( 'not' p) => ( 'not' q)) implies X |- (q => p)

      proof

        assume

         A1: X |- (( 'not' p) => ( 'not' q));

        X |- ((( 'not' p) => ( 'not' q)) => (q => p)) by CQC_THE1: 59;

        hence thesis by A1, CQC_THE1: 55;

      end;

      assume

       A2: X |- (q => p);

      X |- ((q => p) => (( 'not' p) => ( 'not' q))) by CQC_THE1: 59;

      hence thesis by A2, CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:70

    X |- ( 'not' ( 'not' p)) iff X |- p

    proof

      thus X |- ( 'not' ( 'not' p)) implies X |- p

      proof

        assume

         A1: X |- ( 'not' ( 'not' p));

        X |- (( 'not' ( 'not' p)) => p) by CQC_THE1: 59;

        hence thesis by A1, CQC_THE1: 55;

      end;

      assume

       A2: X |- p;

      X |- (p => ( 'not' ( 'not' p))) by CQC_THE1: 59;

      hence thesis by A2, CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:71

    X |- (p => ( 'not' ( 'not' q))) iff X |- (p => q)

    proof

      thus X |- (p => ( 'not' ( 'not' q))) implies X |- (p => q)

      proof

        assume

         A1: X |- (p => ( 'not' ( 'not' q)));

        X |- ((p => ( 'not' ( 'not' q))) => (p => q)) by CQC_THE1: 59;

        hence thesis by A1, CQC_THE1: 55;

      end;

      assume

       A2: X |- (p => q);

      X |- (q => ( 'not' ( 'not' q))) by CQC_THE1: 59;

      hence thesis by A2, Th59;

    end;

    theorem :: LUKASI_1:72

    X |- (( 'not' ( 'not' p)) => q) iff X |- (p => q)

    proof

      thus X |- (( 'not' ( 'not' p)) => q) implies X |- (p => q)

      proof

        assume

         A1: X |- (( 'not' ( 'not' p)) => q);

        X |- ((( 'not' ( 'not' p)) => q) => (p => q)) by CQC_THE1: 59;

        hence thesis by A1, CQC_THE1: 55;

      end;

      assume

       A2: X |- (p => q);

      X |- (( 'not' ( 'not' p)) => p) by CQC_THE1: 59;

      hence thesis by A2, Th59;

    end;

    theorem :: LUKASI_1:73



     Th73: X |- (p => ( 'not' q)) implies X |- (q => ( 'not' p))

    proof

      assume

       A1: X |- (p => ( 'not' q));

      X |- ((p => ( 'not' q)) => (q => ( 'not' p))) by CQC_THE1: 59;

      hence thesis by A1, CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:74



     Th74: X |- (( 'not' p) => q) implies X |- (( 'not' q) => p)

    proof

      assume

       A1: X |- (( 'not' p) => q);

      X |- ((( 'not' p) => q) => (( 'not' q) => p)) by CQC_THE1: 59;

      hence thesis by A1, CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:75

    X |- (p => ( 'not' q)) & X |- q implies X |- ( 'not' p)

    proof

      assume X |- (p => ( 'not' q));

      then X |- (q => ( 'not' p)) by Th73;

      hence thesis by CQC_THE1: 55;

    end;

    theorem :: LUKASI_1:76

    X |- (( 'not' p) => q) & X |- ( 'not' q) implies X |- p

    proof

      assume X |- (( 'not' p) => q);

      then X |- (( 'not' q) => p) by Th74;

      hence thesis by CQC_THE1: 55;

    end;