procal_1.miz

    begin

    reserve A for QC-alphabet;

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

    theorem :: PROCAL_1:1



     Th1: ( 'not' (p '&' ( 'not' p))) in ( TAUT A)

    proof

      (p => p) in ( TAUT A) by LUKASI_1: 4;

      hence thesis by QC_LANG2:def 2;

    end;



     Lm1: (p 'or' q) = (( 'not' p) => q)

    proof

      (( 'not' p) => q) = ( 'not' (( 'not' p) '&' ( 'not' q))) by QC_LANG2:def 2;

      hence thesis by QC_LANG2:def 3;

    end;

    theorem :: PROCAL_1:2



     Th2: (p 'or' ( 'not' p)) in ( TAUT A)

    proof

      (( 'not' p) => ( 'not' p)) in ( TAUT A) by LUKASI_1: 4;

      hence thesis by Lm1;

    end;

    theorem :: PROCAL_1:3



     Th3: (p => (p 'or' q)) in ( TAUT A)

    proof

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

      hence thesis by Lm1;

    end;

    theorem :: PROCAL_1:4



     Th4: (q => (p 'or' q)) in ( TAUT A)

    proof

      (q => (( 'not' p) => q)) in ( TAUT A) by LUKASI_1: 5;

      hence thesis by Lm1;

    end;

    theorem :: PROCAL_1:5



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

    proof

      ((( 'not' p) => q) => (( 'not' p) => q)) in ( TAUT A) by LUKASI_1: 4;

      hence thesis by Lm1;

    end;

    theorem :: PROCAL_1:6



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

    proof

      ( 'not' (p 'or' q)) = ( 'not' ( 'not' (( 'not' p) '&' ( 'not' q)))) by QC_LANG2:def 3;

      hence thesis by LUKASI_1: 25;

    end;

    theorem :: PROCAL_1:7



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

    proof

      ( 'not' (p 'or' q)) = ( 'not' ( 'not' (( 'not' p) '&' ( 'not' q)))) by QC_LANG2:def 3;

      hence thesis by LUKASI_1: 27;

    end;

    theorem :: PROCAL_1:8



     Th8: ((p 'or' q) => (q 'or' p)) in ( TAUT A)

    proof

      ((( 'not' p) => q) => (( 'not' q) => p)) in ( TAUT A) by LUKASI_1: 31;

      then ((p 'or' q) => (( 'not' q) => p)) in ( TAUT A) by Lm1;

      hence thesis by Lm1;

    end;

    theorem :: PROCAL_1:9

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

    proof

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

      hence thesis by Th2, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:10

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

    proof

      ((p => (p 'or' q)) => (( 'not' (p 'or' q)) => ( 'not' p))) in ( TAUT A) & (p => (p 'or' q)) in ( TAUT A) by Th3, LUKASI_1: 26;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:11



     Th11: ((p 'or' p) => p) in ( TAUT A)

    proof

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

      hence thesis by LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:12

    (p => (p 'or' p)) in ( TAUT A) by Th3;

    theorem :: PROCAL_1:13

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

    proof

      (( 'not' q) => ( 'not' (p '&' ( 'not' p)))) in ( TAUT A) by Th1, LUKASI_1: 13;

      hence thesis by LUKASI_1: 35;

    end;

    theorem :: PROCAL_1:14

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

    proof



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

      (( 'not' ( 'not' p)) => q) = (( 'not' p) 'or' q) & (( 'not' ( 'not' p)) => p) in ( TAUT A) by Lm1, LUKASI_1: 25;

      hence thesis by A1, CQC_THE1: 46;

    end;



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

    proof

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

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

      hence thesis by LUKASI_1: 35;

    end;



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

    proof

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

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

      hence thesis by LUKASI_1: 35;

    end;

    theorem :: PROCAL_1:15



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

    proof



       A1: ((p '&' ( 'not' ( 'not' q))) => ( 'not' ( 'not' (p '&' ( 'not' ( 'not' q)))))) in ( TAUT A) by LUKASI_1: 27;

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

      then

       A2: ((p '&' q) => (( 'not' ( 'not' q)) '&' p)) in ( TAUT A) by LUKASI_1: 3;

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

      then ((p '&' q) => (p '&' ( 'not' ( 'not' q)))) in ( TAUT A) by A2, LUKASI_1: 3;

      then ((p '&' q) => ( 'not' ( 'not' (p '&' ( 'not' ( 'not' q)))))) in ( TAUT A) by A1, LUKASI_1: 3;

      hence thesis by QC_LANG2:def 2;

    end;

    theorem :: PROCAL_1:16



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

    proof



       A1: (( 'not' ( 'not' (p '&' ( 'not' ( 'not' q))))) => (p '&' ( 'not' ( 'not' q)))) in ( TAUT A) by LUKASI_1: 25;

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

      then

       A2: ((p '&' ( 'not' ( 'not' q))) => (q '&' p)) in ( TAUT A) by LUKASI_1: 3;

      ((q '&' p) => (p '&' q)) in ( TAUT A) by CQC_THE1: 45;

      then ((p '&' ( 'not' ( 'not' q))) => (p '&' q)) in ( TAUT A) by A2, LUKASI_1: 3;

      then (( 'not' ( 'not' (p '&' ( 'not' ( 'not' q))))) => (p '&' q)) in ( TAUT A) by A1, LUKASI_1: 3;

      hence thesis by QC_LANG2:def 2;

    end;

    theorem :: PROCAL_1:17



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

    proof

      (( 'not' ( 'not' p)) => p) in ( TAUT A) & ((( 'not' ( 'not' p)) => p) => ((p => ( 'not' q)) => (( 'not' ( 'not' p)) => ( 'not' q)))) in ( TAUT A) by LUKASI_1: 1, LUKASI_1: 25;

      then

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

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

      then

       A2: (( 'not' (p '&' q)) => ( 'not' ( 'not' (p => ( 'not' q))))) in ( TAUT A) by LUKASI_1: 34;

      (( 'not' ( 'not' (p => ( 'not' q)))) => (p => ( 'not' q))) in ( TAUT A) by LUKASI_1: 25;

      then (( 'not' (p '&' q)) => (p => ( 'not' q))) in ( TAUT A) by A2, LUKASI_1: 3;

      then (( 'not' (p '&' q)) => (( 'not' ( 'not' p)) => ( 'not' q))) in ( TAUT A) by A1, LUKASI_1: 3;

      hence thesis by Lm1;

    end;

    theorem :: PROCAL_1:18



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

    proof



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

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

      then

       A2: (( 'not' ( 'not' (p => ( 'not' q)))) => ( 'not' (p '&' q))) in ( TAUT A) by LUKASI_1: 34;

      ((p => ( 'not' q)) => ( 'not' ( 'not' (p => ( 'not' q))))) in ( TAUT A) by LUKASI_1: 27;

      then

       A3: ((p => ( 'not' q)) => ( 'not' (p '&' q))) in ( TAUT A) by A2, LUKASI_1: 3;

      (( 'not' p) 'or' ( 'not' q)) = (( 'not' ( 'not' p)) => ( 'not' q)) & (p => ( 'not' ( 'not' p))) in ( TAUT A) by Lm1, LUKASI_1: 27;

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

      hence thesis by A3, LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:19



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

    proof

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

      then

       A1: (( 'not' (( 'not' p) 'or' ( 'not' q))) => ( 'not' ( 'not' p))) in ( TAUT A) by LUKASI_1: 34;

      ((( 'not' p) 'or' ( 'not' q)) => ( 'not' (p '&' q))) in ( TAUT A) by Th18;

      then

       A2: (( 'not' ( 'not' (p '&' q))) => ( 'not' (( 'not' p) 'or' ( 'not' q)))) in ( TAUT A) by LUKASI_1: 34;

      ((p '&' q) => ( 'not' ( 'not' (p '&' q)))) in ( TAUT A) by LUKASI_1: 27;

      then

       A3: ((p '&' q) => ( 'not' (( 'not' p) 'or' ( 'not' q)))) in ( TAUT A) by A2, LUKASI_1: 3;

      (( 'not' ( 'not' p)) => p) in ( TAUT A) by LUKASI_1: 25;

      then (( 'not' (( 'not' p) 'or' ( 'not' q))) => p) in ( TAUT A) by A1, LUKASI_1: 3;

      hence thesis by A3, LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:20



     Th20: ((p '&' q) => (p 'or' q)) in ( TAUT A)

    proof

      (p => (p 'or' q)) in ( TAUT A) & ((p '&' q) => p) in ( TAUT A) by Th3, Th19;

      hence thesis by LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:21



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

    proof

      ((q '&' p) => q) in ( TAUT A) & ((p '&' q) => (q '&' p)) in ( TAUT A) by Th19, CQC_THE1: 45;

      hence thesis by LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:22

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

    proof

      (( 'not' (p '&' p)) => (( 'not' p) 'or' ( 'not' p))) in ( TAUT A) & ((( 'not' p) 'or' ( 'not' p)) => ( 'not' p)) in ( TAUT A) by Th11, Th17;

      then (( 'not' (p '&' p)) => ( 'not' p)) in ( TAUT A) by LUKASI_1: 3;

      hence thesis by LUKASI_1: 35;

    end;

    theorem :: PROCAL_1:23

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

    proof

      (p <=> q) = ((p => q) '&' (q => p)) by QC_LANG2:def 4;

      hence thesis by Th19;

    end;

    theorem :: PROCAL_1:24

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

    proof

      (p <=> q) = ((p => q) '&' (q => p)) by QC_LANG2:def 4;

      hence thesis by Th21;

    end;

    theorem :: PROCAL_1:25



     Th25: (((p 'or' q) 'or' r) => (p 'or' (q 'or' r))) in ( TAUT A)

    proof

      (( 'not' p) => ((( 'not' r) => q) => (( 'not' q) => r))) in ( TAUT A) & ((( 'not' p) => ((( 'not' r) => q) => (( 'not' q) => r))) => ((( 'not' p) => (( 'not' r) => q)) => (( 'not' p) => (( 'not' q) => r)))) in ( TAUT A) by LUKASI_1: 11, LUKASI_1: 13, LUKASI_1: 31;

      then

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

      (((p 'or' q) 'or' r) => (r 'or' (p 'or' q))) in ( TAUT A) & ((r 'or' (p 'or' q)) => (( 'not' r) => (p 'or' q))) in ( TAUT A) by Th5, Th8;

      then (((p 'or' q) 'or' r) => (( 'not' r) => (p 'or' q))) in ( TAUT A) by LUKASI_1: 3;

      then

       A2: (((p 'or' q) 'or' r) => (( 'not' r) => (( 'not' p) => q))) in ( TAUT A) by Lm1;

      ((( 'not' r) => (( 'not' p) => q)) => (( 'not' p) => (( 'not' r) => q))) in ( TAUT A) by LUKASI_1: 8;

      then (((p 'or' q) 'or' r) => (( 'not' p) => (( 'not' r) => q))) in ( TAUT A) by A2, LUKASI_1: 3;

      then (((p 'or' q) 'or' r) => (( 'not' p) => (( 'not' q) => r))) in ( TAUT A) by A1, LUKASI_1: 3;

      then (((p 'or' q) 'or' r) => (( 'not' p) => (q 'or' r))) in ( TAUT A) by Lm1;

      hence thesis by Lm1;

    end;

    theorem :: PROCAL_1:26

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

    proof



       A1: ((( 'not' p) 'or' (( 'not' r) 'or' ( 'not' q))) => ((( 'not' r) 'or' ( 'not' q)) 'or' ( 'not' p))) in ( TAUT A) by Th8;

      (( 'not' (q '&' r)) => (( 'not' q) 'or' ( 'not' r))) in ( TAUT A) & ((( 'not' q) 'or' ( 'not' r)) => (( 'not' r) 'or' ( 'not' q))) in ( TAUT A) by Th8, Th17;

      then (( 'not' (q '&' r)) => (( 'not' r) 'or' ( 'not' q))) in ( TAUT A) by LUKASI_1: 3;

      then

       A2: (( 'not' ( 'not' p)) => (( 'not' (q '&' r)) => (( 'not' r) 'or' ( 'not' q)))) in ( TAUT A) by LUKASI_1: 13;

      ((( 'not' ( 'not' p)) => (( 'not' (q '&' r)) => (( 'not' r) 'or' ( 'not' q)))) => ((( 'not' ( 'not' p)) => ( 'not' (q '&' r))) => (( 'not' ( 'not' p)) => (( 'not' r) 'or' ( 'not' q))))) in ( TAUT A) by LUKASI_1: 11;

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

      then ((( 'not' p) 'or' ( 'not' (q '&' r))) => (( 'not' ( 'not' p)) => (( 'not' r) 'or' ( 'not' q)))) in ( TAUT A) by Lm1;

      then

       A3: ((( 'not' p) 'or' ( 'not' (q '&' r))) => (( 'not' p) 'or' (( 'not' r) 'or' ( 'not' q)))) in ( TAUT A) by Lm1;

      (( 'not' (p '&' (q '&' r))) => (( 'not' p) 'or' ( 'not' (q '&' r)))) in ( TAUT A) by Th17;

      then (( 'not' (p '&' (q '&' r))) => (( 'not' p) 'or' (( 'not' r) 'or' ( 'not' q)))) in ( TAUT A) by A3, LUKASI_1: 3;

      then

       A4: (( 'not' (p '&' (q '&' r))) => ((( 'not' r) 'or' ( 'not' q)) 'or' ( 'not' p))) in ( TAUT A) by A1, LUKASI_1: 3;



       A5: ((( 'not' (p '&' q)) 'or' ( 'not' r)) => ( 'not' ((p '&' q) '&' r))) in ( TAUT A) by Th18;

      ((( 'not' q) 'or' ( 'not' p)) => (( 'not' p) 'or' ( 'not' q))) in ( TAUT A) & ((( 'not' p) 'or' ( 'not' q)) => ( 'not' (p '&' q))) in ( TAUT A) by Th8, Th18;

      then ((( 'not' q) 'or' ( 'not' p)) => ( 'not' (p '&' q))) in ( TAUT A) by LUKASI_1: 3;

      then

       A6: (( 'not' ( 'not' r)) => ((( 'not' q) 'or' ( 'not' p)) => ( 'not' (p '&' q)))) in ( TAUT A) by LUKASI_1: 13;

      ((( 'not' ( 'not' r)) => ((( 'not' q) 'or' ( 'not' p)) => ( 'not' (p '&' q)))) => ((( 'not' ( 'not' r)) => (( 'not' q) 'or' ( 'not' p))) => (( 'not' ( 'not' r)) => ( 'not' (p '&' q))))) in ( TAUT A) by LUKASI_1: 11;

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

      then ((( 'not' r) 'or' (( 'not' q) 'or' ( 'not' p))) => (( 'not' ( 'not' r)) => ( 'not' (p '&' q)))) in ( TAUT A) by Lm1;

      then

       A7: ((( 'not' r) 'or' (( 'not' q) 'or' ( 'not' p))) => (( 'not' r) 'or' ( 'not' (p '&' q)))) in ( TAUT A) by Lm1;

      ((( 'not' r) 'or' ( 'not' (p '&' q))) => (( 'not' (p '&' q)) 'or' ( 'not' r))) in ( TAUT A) by Th8;

      then ((( 'not' r) 'or' (( 'not' q) 'or' ( 'not' p))) => (( 'not' (p '&' q)) 'or' ( 'not' r))) in ( TAUT A) by A7, LUKASI_1: 3;

      then

       A8: ((( 'not' r) 'or' (( 'not' q) 'or' ( 'not' p))) => ( 'not' ((p '&' q) '&' r))) in ( TAUT A) by A5, LUKASI_1: 3;

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

      then (( 'not' (p '&' (q '&' r))) => (( 'not' r) 'or' (( 'not' q) 'or' ( 'not' p)))) in ( TAUT A) by A4, LUKASI_1: 3;

      then (( 'not' (p '&' (q '&' r))) => ( 'not' ((p '&' q) '&' r))) in ( TAUT A) by A8, LUKASI_1: 3;

      hence thesis by LUKASI_1: 35;

    end;

    theorem :: PROCAL_1:27



     Th27: ((p 'or' (q 'or' r)) => ((p 'or' q) 'or' r)) in ( TAUT A)

    proof



       A1: ((( 'not' p) => (( 'not' r) => q)) => (( 'not' r) => (( 'not' p) => q))) in ( TAUT A) by LUKASI_1: 8;

      (( 'not' p) => ((( 'not' q) => r) => (( 'not' r) => q))) in ( TAUT A) & ((( 'not' p) => ((( 'not' q) => r) => (( 'not' r) => q))) => ((( 'not' p) => (( 'not' q) => r)) => (( 'not' p) => (( 'not' r) => q)))) in ( TAUT A) by LUKASI_1: 11, LUKASI_1: 13, LUKASI_1: 31;

      then

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

      ((p 'or' (q 'or' r)) => (( 'not' p) => (q 'or' r))) in ( TAUT A) by Th5;

      then ((p 'or' (q 'or' r)) => (( 'not' p) => (( 'not' q) => r))) in ( TAUT A) by Lm1;

      then ((p 'or' (q 'or' r)) => (( 'not' p) => (( 'not' r) => q))) in ( TAUT A) by A2, LUKASI_1: 3;

      then ((p 'or' (q 'or' r)) => (( 'not' r) => (( 'not' p) => q))) in ( TAUT A) by A1, LUKASI_1: 3;

      then

       A3: ((p 'or' (q 'or' r)) => (r 'or' (( 'not' p) => q))) in ( TAUT A) by Lm1;

      ((r 'or' (( 'not' p) => q)) => ((( 'not' p) => q) 'or' r)) in ( TAUT A) by Th8;

      then ((p 'or' (q 'or' r)) => ((( 'not' p) => q) 'or' r)) in ( TAUT A) by A3, LUKASI_1: 3;

      hence thesis by Lm1;

    end;

    theorem :: PROCAL_1:28



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

    proof



       A1: ((((p '&' q) 'or' ( 'not' p)) 'or' ( 'not' q)) => (( 'not' q) 'or' ((p '&' q) 'or' ( 'not' p)))) in ( TAUT A) by Th8;

      (( 'not' (p '&' q)) => (( 'not' p) 'or' ( 'not' q))) in ( TAUT A) by Th17;

      then

       A2: ((p '&' q) 'or' (( 'not' p) 'or' ( 'not' q))) in ( TAUT A) by Lm1;

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

      then (((p '&' q) 'or' ( 'not' p)) 'or' ( 'not' q)) in ( TAUT A) by A2, CQC_THE1: 46;

      then (( 'not' q) 'or' ((p '&' q) 'or' ( 'not' p))) in ( TAUT A) by A1, CQC_THE1: 46;

      then

       A3: (( 'not' ( 'not' q)) => ((p '&' q) 'or' ( 'not' p))) in ( TAUT A) by Lm1;

      (q => (((p '&' q) 'or' ( 'not' p)) => (( 'not' p) 'or' (p '&' q)))) in ( TAUT A) & ((q => (((p '&' q) 'or' ( 'not' p)) => (( 'not' p) 'or' (p '&' q)))) => ((q => ((p '&' q) 'or' ( 'not' p))) => (q => (( 'not' p) 'or' (p '&' q))))) in ( TAUT A) by Th8, LUKASI_1: 11, LUKASI_1: 13;

      then

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

      (q => ( 'not' ( 'not' q))) in ( TAUT A) by LUKASI_1: 27;

      then (q => ((p '&' q) 'or' ( 'not' p))) in ( TAUT A) by A3, LUKASI_1: 3;

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

      then (q => (( 'not' ( 'not' p)) => (p '&' q))) in ( TAUT A) by Lm1;

      then

       A5: (( 'not' ( 'not' p)) => (q => (p '&' q))) in ( TAUT A) by LUKASI_1: 15;

      (p => ( 'not' ( 'not' p))) in ( TAUT A) by LUKASI_1: 27;

      hence thesis by A5, LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:29

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

    proof

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

      hence thesis by QC_LANG2:def 4;

    end;



     Lm4: p in ( TAUT A) & q in ( TAUT A) implies (p '&' q) in ( TAUT A)

    proof

      assume that

       A1: p in ( TAUT A) and

       A2: q in ( TAUT A);

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

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

      hence thesis by A2, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:30

    ((p 'or' q) <=> (q 'or' p)) in ( TAUT A)

    proof

      set P = (p 'or' q);

      set Q = (q 'or' p);

      (P => Q) in ( TAUT A) & (Q => P) in ( TAUT A) by Th8;

      then ((P => Q) '&' (Q => P)) in ( TAUT A) by Lm4;

      hence thesis by QC_LANG2:def 4;

    end;

    theorem :: PROCAL_1:31

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

    proof

      (p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r)))) in ( TAUT A) & (p => (q => (p '&' q))) in ( TAUT A) by Th28, LUKASI_1: 1, LUKASI_1: 13;

      then

       A1: (p => (((p '&' q) => r) => (q => r))) in ( TAUT A) by LUKASI_1: 20;

      ((p => (((p '&' q) => r) => (q => r))) => (((p '&' q) => r) => (p => (q => r)))) in ( TAUT A) by LUKASI_1: 8;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:32



     Th32: ((p => (q => r)) => ((p '&' q) => r)) in ( TAUT A)

    proof



       A1: ((p => ((p '&' q) => r)) => ((p '&' q) => (p => r))) in ( TAUT A) by LUKASI_1: 8;

      (((p '&' q) => (p => r)) => (((p '&' q) => p) => ((p '&' q) => r))) in ( TAUT A) by LUKASI_1: 11;

      then

       A2: (((p '&' q) => (p => r)) => ((p '&' q) => r)) in ( TAUT A) by Th19, LUKASI_1: 16;

      ((p '&' q) => q) in ( TAUT A) & (((p '&' q) => q) => ((q => r) => ((p '&' q) => r))) in ( TAUT A) by Th21, LUKASI_1: 1;

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

      then

       A3: (p => ((q => r) => ((p '&' q) => r))) in ( TAUT A) by LUKASI_1: 13;

      ((p => ((q => r) => ((p '&' q) => r))) => ((p => (q => r)) => (p => ((p '&' q) => r)))) in ( TAUT A) by LUKASI_1: 11;

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

      then ((p => (q => r)) => ((p '&' q) => (p => r))) in ( TAUT A) by A1, LUKASI_1: 3;

      hence thesis by A2, LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:33



     Th33: ((r => p) => ((r => q) => (r => (p '&' q)))) in ( TAUT A)

    proof

      (r => (p => (q => (p '&' q)))) in ( TAUT A) & ((r => (p => (q => (p '&' q)))) => ((r => p) => (r => (q => (p '&' q))))) in ( TAUT A) by Th28, LUKASI_1: 11, LUKASI_1: 13;

      then

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

      ((r => (q => (p '&' q))) => ((r => q) => (r => (p '&' q)))) in ( TAUT A) by LUKASI_1: 11;

      hence thesis by A1, LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:34

    (((p 'or' q) => r) => ((p => r) 'or' (q => r))) in ( TAUT A)

    proof

      (q => (p 'or' q)) in ( TAUT A) & ((q => (p 'or' q)) => (((p 'or' q) => r) => (q => r))) in ( TAUT A) by Th4, LUKASI_1: 1;

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

      then (( 'not' (p => r)) => (((p 'or' q) => r) => (q => r))) in ( TAUT A) by LUKASI_1: 13;

      then (((p 'or' q) => r) => (( 'not' (p => r)) => (q => r))) in ( TAUT A) by LUKASI_1: 15;

      hence thesis by Lm1;

    end;

    theorem :: PROCAL_1:35



     Th35: ((p => r) => ((q => r) => ((p 'or' q) => r))) in ( TAUT A)

    proof

      set AA = (( 'not' r) => ( 'not' p));

      set B = (( 'not' r) => ( 'not' q));

      set C = (( 'not' r) => (( 'not' p) '&' ( 'not' q)));

      set D = ((p 'or' q) => r);

      set E = (q => r);



       A1: (AA => (B => C)) in ( TAUT A) by Th33;

      (C => (( 'not' (( 'not' p) '&' ( 'not' q))) => r)) in ( TAUT A) by LUKASI_1: 31;

      then (C => D) in ( TAUT A) by QC_LANG2:def 3;

      then

       A2: (B => (C => D)) in ( TAUT A) by LUKASI_1: 13;

      ((B => (C => D)) => ((B => C) => (B => D))) in ( TAUT A) by LUKASI_1: 11;

      then ((B => C) => (B => D)) in ( TAUT A) by A2, CQC_THE1: 46;

      then (AA => (B => D)) in ( TAUT A) by A1, LUKASI_1: 3;

      then

       A3: (B => (AA => D)) in ( TAUT A) by LUKASI_1: 15;

      (E => B) in ( TAUT A) by LUKASI_1: 26;

      then (E => (AA => D)) in ( TAUT A) by A3, LUKASI_1: 3;

      then

       A4: (AA => (E => D)) in ( TAUT A) by LUKASI_1: 15;

      ((p => r) => AA) in ( TAUT A) by LUKASI_1: 26;

      hence thesis by A4, LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:36



     Th36: (((p => r) '&' (q => r)) => ((p 'or' q) => r)) in ( TAUT A)

    proof

      set P = (p => r);

      set Q = (q => r);

      set R = ((p 'or' q) => r);

      (P => (Q => R)) in ( TAUT A) & ((P => (Q => R)) => ((P '&' Q) => R)) in ( TAUT A) by Th32, Th35;

      hence thesis by CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:37

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

    proof

      (p => ( 'not' (q '&' ( 'not' q)))) in ( TAUT A) by Th1, LUKASI_1: 13;

      then

       A1: (( 'not' ( 'not' (q '&' ( 'not' q)))) => ( 'not' p)) in ( TAUT A) by LUKASI_1: 34;

      ((q '&' ( 'not' q)) => ( 'not' ( 'not' (q '&' ( 'not' q))))) in ( TAUT A) by LUKASI_1: 27;

      then ((q '&' ( 'not' q)) => ( 'not' p)) in ( TAUT A) by A1, LUKASI_1: 3;

      then

       A2: (p => ((q '&' ( 'not' q)) => ( 'not' p))) in ( TAUT A) by LUKASI_1: 13;

      (( 'not' ( 'not' p)) => p) in ( TAUT A) & ((( 'not' ( 'not' p)) => p) => ((p => ( 'not' p)) => (( 'not' ( 'not' p)) => ( 'not' p)))) in ( TAUT A) by LUKASI_1: 1, LUKASI_1: 25;

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

      then

       A3: ((p => ( 'not' p)) => ( 'not' p)) in ( TAUT A) by LUKASI_1: 3;

      ((p => ((q '&' ( 'not' q)) => ( 'not' p))) => ((p => (q '&' ( 'not' q))) => (p => ( 'not' p)))) in ( TAUT A) by LUKASI_1: 11;

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

      hence thesis by A3, LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:38

    (((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r))) in ( TAUT A)

    proof

      ((( 'not' p) => q) => ((( 'not' p) => r) => (( 'not' p) => (q '&' r)))) in ( TAUT A) by Th33;

      then ((p 'or' q) => ((( 'not' p) => r) => (( 'not' p) => (q '&' r)))) in ( TAUT A) by Lm1;

      then ((p 'or' q) => ((p 'or' r) => (( 'not' p) => (q '&' r)))) in ( TAUT A) by Lm1;

      then

       A1: ((p 'or' q) => ((p 'or' r) => (p 'or' (q '&' r)))) in ( TAUT A) by Lm1;

      (((p 'or' q) => ((p 'or' r) => (p 'or' (q '&' r)))) => (((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)))) in ( TAUT A) by Th32;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:39

    ((p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r))) in ( TAUT A)

    proof



       A1: (( 'not' ((p '&' q) 'or' (p '&' r))) => (( 'not' (p '&' q)) '&' ( 'not' (p '&' r)))) in ( TAUT A) by Th6;

      (( 'not' (p => ( 'not' q))) => (p '&' q)) in ( TAUT A) & ((( 'not' (p => ( 'not' q))) => (p '&' q)) => (( 'not' (p '&' q)) => (p => ( 'not' q)))) in ( TAUT A) by Th16, LUKASI_1: 31;

      then

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

      (( 'not' (p => ( 'not' r))) => (p '&' r)) in ( TAUT A) & ((( 'not' (p => ( 'not' r))) => (p '&' r)) => (( 'not' (p '&' r)) => (p => ( 'not' r)))) in ( TAUT A) by Th16, LUKASI_1: 31;

      then

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

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

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

      then (( 'not' (p '&' q)) => ((p => ( 'not' r)) => ( 'not' (p '&' (q 'or' r))))) in ( TAUT A) by A2, LUKASI_1: 3;

      then ((p => ( 'not' r)) => (( 'not' (p '&' q)) => ( 'not' (p '&' (q 'or' r))))) in ( TAUT A) by LUKASI_1: 15;

      then (( 'not' (p '&' r)) => (( 'not' (p '&' q)) => ( 'not' (p '&' (q 'or' r))))) in ( TAUT A) by A3, LUKASI_1: 3;

      then

       A4: (( 'not' (p '&' q)) => (( 'not' (p '&' r)) => ( 'not' (p '&' (q 'or' r))))) in ( TAUT A) by LUKASI_1: 15;

      ((( 'not' (p '&' q)) => (( 'not' (p '&' r)) => ( 'not' (p '&' (q 'or' r))))) => ((( 'not' (p '&' q)) '&' ( 'not' (p '&' r))) => ( 'not' (p '&' (q 'or' r))))) in ( TAUT A) by Th32;

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

      then (( 'not' ((p '&' q) 'or' (p '&' r))) => ( 'not' (p '&' (q 'or' r)))) in ( TAUT A) by A1, LUKASI_1: 3;

      hence thesis by LUKASI_1: 35;

    end;

    theorem :: PROCAL_1:40



     Th40: (((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r)) in ( TAUT A)

    proof

      (((( 'not' p) => r) '&' (( 'not' q) => r)) => ((( 'not' p) 'or' ( 'not' q)) => r)) in ( TAUT A) by Th36;

      then (((p 'or' r) '&' (( 'not' q) => r)) => ((( 'not' p) 'or' ( 'not' q)) => r)) in ( TAUT A) by Lm1;

      then

       A1: (((p 'or' r) '&' (q 'or' r)) => ((( 'not' p) 'or' ( 'not' q)) => r)) in ( TAUT A) by Lm1;

      (( 'not' (p '&' q)) => (( 'not' p) 'or' ( 'not' q))) in ( TAUT A) & ((( 'not' (p '&' q)) => (( 'not' p) 'or' ( 'not' q))) => (((( 'not' p) 'or' ( 'not' q)) => r) => (( 'not' (p '&' q)) => r))) in ( TAUT A) by Th17, LUKASI_1: 1;

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

      then (((p 'or' r) '&' (q 'or' r)) => (( 'not' (p '&' q)) => r)) in ( TAUT A) by A1, LUKASI_1: 3;

      hence thesis by Lm1;

    end;



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

    proof



       A1: (( 'not' (r => ( 'not' q))) => (r '&' q)) in ( TAUT A) by Th16;

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

      then (( 'not' q) => ( 'not' p)) in ( TAUT A) by LUKASI_1: 34;

      then

       A2: (r => (( 'not' q) => ( 'not' p))) in ( TAUT A) by LUKASI_1: 13;

      ((r => (( 'not' q) => ( 'not' p))) => ((r => ( 'not' q)) => (r => ( 'not' p)))) in ( TAUT A) by LUKASI_1: 11;

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

      then

       A3: (( 'not' (r => ( 'not' p))) => ( 'not' (r => ( 'not' q)))) in ( TAUT A) by LUKASI_1: 34;

      ((r '&' p) => ( 'not' (r => ( 'not' p)))) in ( TAUT A) by Th15;

      then ((r '&' p) => ( 'not' (r => ( 'not' q)))) in ( TAUT A) by A3, LUKASI_1: 3;

      hence thesis by A1, LUKASI_1: 3;

    end;



     Lm6: (p => q) in ( TAUT A) implies ((p 'or' r) => (q 'or' r)) in ( TAUT A)

    proof

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

      then

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

      ((( 'not' q) => ( 'not' p)) => ((( 'not' p) => r) => (( 'not' q) => r))) in ( TAUT A) by LUKASI_1: 1;

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

      then ((p 'or' r) => (( 'not' q) => r)) in ( TAUT A) by Lm1;

      hence thesis by Lm1;

    end;



     Lm7: (p => q) in ( TAUT A) implies ((r 'or' p) => (r 'or' q)) in ( TAUT A)

    proof

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

      then

       A1: (( 'not' r) => (p => q)) in ( TAUT A) by LUKASI_1: 13;

      ((( 'not' r) => (p => q)) => ((( 'not' r) => p) => (( 'not' r) => q))) in ( TAUT A) by LUKASI_1: 11;

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

      then ((r 'or' p) => (( 'not' r) => q)) in ( TAUT A) by Lm1;

      hence thesis by Lm1;

    end;

    theorem :: PROCAL_1:41

    (((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r))) in ( TAUT A)

    proof



       A1: (( 'not' ((( 'not' p) 'or' ( 'not' r)) '&' (( 'not' q) 'or' ( 'not' r)))) => (( 'not' (( 'not' p) 'or' ( 'not' r))) 'or' ( 'not' (( 'not' q) 'or' ( 'not' r))))) in ( TAUT A) by Th17;

      (((( 'not' p) 'or' ( 'not' r)) '&' (( 'not' q) 'or' ( 'not' r))) => ((( 'not' p) '&' ( 'not' q)) 'or' ( 'not' r))) in ( TAUT A) by Th40;

      then

       A2: (( 'not' ((( 'not' p) '&' ( 'not' q)) 'or' ( 'not' r))) => ( 'not' ((( 'not' p) 'or' ( 'not' r)) '&' (( 'not' q) 'or' ( 'not' r))))) in ( TAUT A) by LUKASI_1: 34;

      ((( 'not' (( 'not' p) '&' ( 'not' q))) '&' ( 'not' ( 'not' r))) => ( 'not' ((( 'not' p) '&' ( 'not' q)) 'or' ( 'not' r)))) in ( TAUT A) by Th7;

      then ((( 'not' (( 'not' p) '&' ( 'not' q))) '&' ( 'not' ( 'not' r))) => ( 'not' ((( 'not' p) 'or' ( 'not' r)) '&' (( 'not' q) 'or' ( 'not' r))))) in ( TAUT A) by A2, LUKASI_1: 3;

      then

       A3: (((p 'or' q) '&' ( 'not' ( 'not' r))) => ( 'not' ((( 'not' p) 'or' ( 'not' r)) '&' (( 'not' q) 'or' ( 'not' r))))) in ( TAUT A) by QC_LANG2:def 3;

      (( 'not' (p '&' r)) => (( 'not' p) 'or' ( 'not' r))) in ( TAUT A) & ((( 'not' (p '&' r)) => (( 'not' p) 'or' ( 'not' r))) => (( 'not' (( 'not' p) 'or' ( 'not' r))) => (p '&' r))) in ( TAUT A) by Th17, LUKASI_1: 31;

      then (( 'not' (( 'not' p) 'or' ( 'not' r))) => (p '&' r)) in ( TAUT A) by CQC_THE1: 46;

      then

       A4: ((( 'not' (( 'not' p) 'or' ( 'not' r))) 'or' ( 'not' (( 'not' q) 'or' ( 'not' r)))) => ((p '&' r) 'or' ( 'not' (( 'not' q) 'or' ( 'not' r))))) in ( TAUT A) by Lm6;

      (( 'not' (q '&' r)) => (( 'not' q) 'or' ( 'not' r))) in ( TAUT A) & ((( 'not' (q '&' r)) => (( 'not' q) 'or' ( 'not' r))) => (( 'not' (( 'not' q) 'or' ( 'not' r))) => (q '&' r))) in ( TAUT A) by Th17, LUKASI_1: 31;

      then (( 'not' (( 'not' q) 'or' ( 'not' r))) => (q '&' r)) in ( TAUT A) by CQC_THE1: 46;

      then

       A5: (((p '&' r) 'or' ( 'not' (( 'not' q) 'or' ( 'not' r)))) => ((p '&' r) 'or' (q '&' r))) in ( TAUT A) by Lm7;

      (r => ( 'not' ( 'not' r))) in ( TAUT A) by LUKASI_1: 27;

      then (((p 'or' q) '&' r) => ((p 'or' q) '&' ( 'not' ( 'not' r)))) in ( TAUT A) by Lm5;

      then (((p 'or' q) '&' r) => ( 'not' ((( 'not' p) 'or' ( 'not' r)) '&' (( 'not' q) 'or' ( 'not' r))))) in ( TAUT A) by A3, LUKASI_1: 3;

      then (((p 'or' q) '&' r) => (( 'not' (( 'not' p) 'or' ( 'not' r))) 'or' ( 'not' (( 'not' q) 'or' ( 'not' r))))) in ( TAUT A) by A1, LUKASI_1: 3;

      then (((p 'or' q) '&' r) => ((p '&' r) 'or' ( 'not' (( 'not' q) 'or' ( 'not' r))))) in ( TAUT A) by A4, LUKASI_1: 3;

      hence thesis by A5, LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:42

    p in ( TAUT A) implies (p 'or' q) in ( TAUT A)

    proof

      assume

       A1: p in ( TAUT A);

      (p => (p 'or' q)) in ( TAUT A) by Th3;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:43

    q in ( TAUT A) implies (p 'or' q) in ( TAUT A)

    proof

      assume

       A1: q in ( TAUT A);

      (q => (p 'or' q)) in ( TAUT A) by Th4;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:44

    (p '&' q) in ( TAUT A) implies p in ( TAUT A)

    proof

      assume

       A1: (p '&' q) in ( TAUT A);

      ((p '&' q) => p) in ( TAUT A) by Th19;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:45

    (p '&' q) in ( TAUT A) implies q in ( TAUT A)

    proof

      assume

       A1: (p '&' q) in ( TAUT A);

      ((p '&' q) => q) in ( TAUT A) by Th21;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:46

    (p '&' q) in ( TAUT A) implies (p 'or' q) in ( TAUT A)

    proof

      assume

       A1: (p '&' q) in ( TAUT A);

      ((p '&' q) => (p 'or' q)) in ( TAUT A) by Th20;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:47

    p in ( TAUT A) & q in ( TAUT A) implies (p '&' q) in ( TAUT A) by Lm4;

    theorem :: PROCAL_1:48

    (p => q) in ( TAUT A) implies ((p 'or' r) => (q 'or' r)) in ( TAUT A) by Lm6;

    theorem :: PROCAL_1:49

    (p => q) in ( TAUT A) implies ((r 'or' p) => (r 'or' q)) in ( TAUT A) by Lm7;

    theorem :: PROCAL_1:50

    (p => q) in ( TAUT A) implies ((r '&' p) => (r '&' q)) in ( TAUT A) by Lm5;

    theorem :: PROCAL_1:51



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

    proof



       A1: ((p => q) => ((q => ( 'not' r)) => (p => ( 'not' r)))) in ( TAUT A) by LUKASI_1: 1;

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

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

      then

       A2: (( 'not' (p => ( 'not' r))) => ( 'not' (q => ( 'not' r)))) in ( TAUT A) by LUKASI_1: 34;



       A3: (( 'not' (q => ( 'not' r))) => (q '&' r)) in ( TAUT A) by Th16;

      ((p '&' r) => ( 'not' (p => ( 'not' r)))) in ( TAUT A) by Th15;

      then ((p '&' r) => ( 'not' (q => ( 'not' r)))) in ( TAUT A) by A2, LUKASI_1: 3;

      hence thesis by A3, LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:52

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

    proof

      assume that

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

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

      ((r => p) => ((r => q) => (r => (p '&' q)))) in ( TAUT A) by Th33;

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

      hence thesis by A2, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:53

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

    proof

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

      then

       A1: ((p => r) '&' (q => r)) in ( TAUT A) by Lm4;

      (((p => r) '&' (q => r)) => ((p 'or' q) => r)) in ( TAUT A) by Th36;

      hence thesis by A1, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:54

    (p 'or' q) in ( TAUT A) & ( 'not' p) in ( TAUT A) implies q in ( TAUT A)

    proof

      assume that

       A1: (p 'or' q) in ( TAUT A) and

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

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

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

      hence thesis by A2, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:55

    (p 'or' q) in ( TAUT A) & ( 'not' q) in ( TAUT A) implies p in ( TAUT A)

    proof

      assume that

       A1: (p 'or' q) in ( TAUT A) and

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

      ((q 'or' p) => (( 'not' q) => p)) in ( TAUT A) & ((p 'or' q) => (q 'or' p)) in ( TAUT A) by Th5, Th8;

      then ((p 'or' q) => (( 'not' q) => p)) in ( TAUT A) by LUKASI_1: 3;

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

      hence thesis by A2, CQC_THE1: 46;

    end;

    theorem :: PROCAL_1:56

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

    proof

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

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

      hence thesis by LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:57

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

    proof

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

      then ((p 'or' r) => (q 'or' r)) in ( TAUT A) & ((q 'or' r) => (q 'or' s)) in ( TAUT A) by Lm6, Lm7;

      hence thesis by LUKASI_1: 3;

    end;

    theorem :: PROCAL_1:58

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

    proof



       A1: ( 'not' (p '&' ( 'not' q))) = (p => q) by QC_LANG2:def 2;

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

      then

       A2: (( 'not' ( 'not' p)) => ( 'not' (p '&' ( 'not' q)))) in ( TAUT A) by LUKASI_1: 34;

      (p => ( 'not' ( 'not' p))) in ( TAUT A) by LUKASI_1: 27;

      then (p => ( 'not' (p '&' ( 'not' q)))) in ( TAUT A) by A2, LUKASI_1: 3;

      hence thesis by A1, LUKASI_1: 18;

    end;