:: Calculus of Propositions
::  by Jan Popio{\l}ek and Andrzej Trybulec
::
:: Received October 23, 1990
:: Copyright (c) 1990-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies SUBSET_1, CQC_LANG, XBOOLEAN, CQC_THE1, QC_LANG1;
 notations SUBSET_1, QC_LANG1, CQC_LANG, CQC_THE1;
 constructors CQC_THE1;
 registrations CQC_LANG;
 theorems CQC_THE1, QC_LANG2, LUKASI_1;

begin :: Tautologies

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

theorem 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 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 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 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 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 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 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 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
  '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
  '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 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
  p => ( p 'or' p ) in TAUT(A) by Th3;

theorem
  ( 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
  ( 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 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 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 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,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 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 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 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 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
  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
  ( 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
  ( 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 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,13,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
  (( 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 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,13,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 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,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
  ( 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
  ( 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
  (( 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,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 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 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,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
  (( 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 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 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
  ( 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,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,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
  (( 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
  ( 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 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
  (( 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;

:: Deduction Rules

theorem
  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
  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
  ( 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
  ( 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
  ( 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
  p in TAUT(A) & q in TAUT(A) implies p '&' q in TAUT(A) by Lm4;

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

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

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

theorem 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
  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
  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
  ( 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
  ( 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
  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
  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
  ( 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;