:: PROCAL_1 semantic presentation

begin


theorem Th1: :: PROCAL_1:1
for A being QC-alphabet
for p being Element of CQC-WFF A holds 'not' (p '&' ('not' p)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds 'not' (p '&' ('not' p)) in TAUT A
let p be Element of CQC-WFF A; ::_thesis: 'not' (p '&' ('not' p)) in TAUT A
 p => p in TAUT A by LUKASI_1:4;
hence  'not' (p '&' ('not' p)) in TAUT A by QC_LANG2:def_2; ::_thesis: verum
end;

Lm1:  for A being QC-alphabet
for p, q being Element of CQC-WFF A holds p 'or' q = ('not' p) => q
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds p 'or' q = ('not' p) => q
let p, q be Element of CQC-WFF A; ::_thesis: p 'or' q = ('not' p) => q
 ('not' p) => q = 'not' (('not' p) '&' ('not' q)) by QC_LANG2:def_2;
hence  p 'or' q = ('not' p) => q by QC_LANG2:def_3; ::_thesis: verum
end;

theorem Th2: :: PROCAL_1:2
for A being QC-alphabet
for p being Element of CQC-WFF A holds p 'or' ('not' p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds p 'or' ('not' p) in TAUT A
let p be Element of CQC-WFF A; ::_thesis: p 'or' ('not' p) in TAUT A
 ('not' p) => ('not' p) in TAUT A by LUKASI_1:4;
hence  p 'or' ('not' p) in TAUT A by Lm1; ::_thesis: verum
end;

theorem Th3: :: PROCAL_1:3
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds p => (p 'or' q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds p => (p 'or' q) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: p => (p 'or' q) in TAUT A
 p => (('not' p) => q) in TAUT A by CQC_THE1:43;
hence  p => (p 'or' q) in TAUT A by Lm1; ::_thesis: verum
end;

theorem Th4: :: PROCAL_1:4
for A being QC-alphabet
for q, p being Element of CQC-WFF A holds q => (p 'or' q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A holds q => (p 'or' q) in TAUT A
let q, p be Element of CQC-WFF A; ::_thesis: q => (p 'or' q) in TAUT A
 q => (('not' p) => q) in TAUT A by LUKASI_1:5;
hence  q => (p 'or' q) in TAUT A by Lm1; ::_thesis: verum
end;

theorem Th5: :: PROCAL_1:5
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p 'or' q) => (('not' p) => q) in TAUT A
 (('not' p) => q) => (('not' p) => q) in TAUT A by LUKASI_1:4;
hence  (p 'or' q) => (('not' p) => q) in TAUT A by Lm1; ::_thesis: verum
end;

theorem Th6: :: PROCAL_1:6
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) in TAUT A
 'not' (p 'or' q) = 'not' ('not' (('not' p) '&' ('not' q))) by QC_LANG2:def_3;
hence  ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) in TAUT A by LUKASI_1:25; ::_thesis: verum
end;

theorem Th7: :: PROCAL_1:7
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) in TAUT A
 'not' (p 'or' q) = 'not' ('not' (('not' p) '&' ('not' q))) by QC_LANG2:def_3;
hence  (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) in TAUT A by LUKASI_1:27; ::_thesis: verum
end;

theorem Th8: :: PROCAL_1:8
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p 'or' q) => (q 'or' p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p 'or' q) => (q 'or' p) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p 'or' q) => (q 'or' p) in TAUT A
 (('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  (p 'or' q) => (q 'or' p) in TAUT A by Lm1; ::_thesis: verum
end;

theorem :: PROCAL_1:9
for A being QC-alphabet
for p being Element of CQC-WFF A holds ('not' p) 'or' p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds ('not' p) 'or' p in TAUT A
let p be Element of CQC-WFF A; ::_thesis: ('not' p) 'or' p in TAUT A
 (p 'or' ('not' p)) => (('not' p) 'or' p) in TAUT A by Th8;
hence  ('not' p) 'or' p in TAUT A by Th2, CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:10
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds ('not' (p 'or' q)) => ('not' p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ('not' (p 'or' q)) => ('not' p) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ('not' (p 'or' q)) => ('not' p) in TAUT A
 ( (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  ('not' (p 'or' q)) => ('not' p) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;

theorem Th11: :: PROCAL_1:11
for A being QC-alphabet
for p being Element of CQC-WFF A holds (p 'or' p) => p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds (p 'or' p) => p in TAUT A
let p be Element of CQC-WFF A; ::_thesis: (p 'or' p) => p in TAUT A
 ( (p 'or' p) => (('not' p) => p) in TAUT A & (('not' p) => p) => p in TAUT A ) by Th5, CQC_THE1:42;
hence  (p 'or' p) => p in TAUT A by LUKASI_1:3; ::_thesis: verum
end;

theorem :: PROCAL_1:12
for A being QC-alphabet
for p being Element of CQC-WFF A holds p => (p 'or' p) in TAUT A by Th3;

theorem :: PROCAL_1:13
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p '&' ('not' p)) => q in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p '&' ('not' p)) => q in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p '&' ('not' p)) => q in TAUT A
 ('not' q) => ('not' (p '&' ('not' p))) in TAUT A by Th1, LUKASI_1:13;
hence  (p '&' ('not' p)) => q in TAUT A by LUKASI_1:35; ::_thesis: verum
end;

theorem :: PROCAL_1:14
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p => q) => (('not' p) 'or' q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p => q) => (('not' p) 'or' q) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p => q) => (('not' p) 'or' q) in TAUT A
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  (p => q) => (('not' p) 'or' q) in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;

Lm2:  for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p '&' q) => (('not' ('not' p)) '&' q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p '&' q) => (('not' ('not' p)) '&' q) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p '&' q) => (('not' ('not' p)) '&' q) in TAUT A
 ( (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  (p '&' q) => (('not' ('not' p)) '&' q) in TAUT A by LUKASI_1:35; ::_thesis: verum
end;

Lm3:  for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' ('not' p)) '&' q) => (p '&' q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (('not' ('not' p)) '&' q) => (p '&' q) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (('not' ('not' p)) '&' q) => (p '&' q) in TAUT A
 ( (('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  (('not' ('not' p)) '&' q) => (p '&' q) in TAUT A by LUKASI_1:35; ::_thesis: verum
end;

theorem Th15: :: PROCAL_1:15
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p '&' q) => ('not' (p => ('not' q))) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p '&' q) => ('not' (p => ('not' q))) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p '&' q) => ('not' (p => ('not' q))) in TAUT A
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  (p '&' q) => ('not' (p => ('not' q))) in TAUT A by QC_LANG2:def_2; ::_thesis: verum
end;

theorem Th16: :: PROCAL_1:16
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds ('not' (p => ('not' q))) => (p '&' q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ('not' (p => ('not' q))) => (p '&' q) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ('not' (p => ('not' q))) => (p '&' q) in TAUT A
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  ('not' (p => ('not' q))) => (p '&' q) in TAUT A by QC_LANG2:def_2; ::_thesis: verum
end;

theorem Th17: :: PROCAL_1:17
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT A
 ( ('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  ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT A by Lm1; ::_thesis: verum
end;

theorem Th18: :: PROCAL_1:18
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT A
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  (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT A by A3, LUKASI_1:3; ::_thesis: verum
end;

theorem Th19: :: PROCAL_1:19
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p '&' q) => p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p '&' q) => p in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p '&' q) => p in TAUT A
 ('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  (p '&' q) => p in TAUT A by A3, LUKASI_1:3; ::_thesis: verum
end;

theorem Th20: :: PROCAL_1:20
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p '&' q) => (p 'or' q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p '&' q) => (p 'or' q) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p '&' q) => (p 'or' q) in TAUT A
 ( p => (p 'or' q) in TAUT A & (p '&' q) => p in TAUT A ) by Th3, Th19;
hence  (p '&' q) => (p 'or' q) in TAUT A by LUKASI_1:3; ::_thesis: verum
end;

theorem Th21: :: PROCAL_1:21
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p '&' q) => q in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p '&' q) => q in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p '&' q) => q in TAUT A
 ( (q '&' p) => q in TAUT A & (p '&' q) => (q '&' p) in TAUT A ) by Th19, CQC_THE1:45;
hence  (p '&' q) => q in TAUT A by LUKASI_1:3; ::_thesis: verum
end;

theorem :: PROCAL_1:22
for A being QC-alphabet
for p being Element of CQC-WFF A holds p => (p '&' p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds p => (p '&' p) in TAUT A
let p be Element of CQC-WFF A; ::_thesis: p => (p '&' p) in TAUT A
 ( ('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  p => (p '&' p) in TAUT A by LUKASI_1:35; ::_thesis: verum
end;

theorem :: PROCAL_1:23
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p <=> q) => (p => q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p <=> q) => (p => q) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p <=> q) => (p => q) in TAUT A
 p <=> q = (p => q) '&' (q => p) by QC_LANG2:def_4;
hence  (p <=> q) => (p => q) in TAUT A by Th19; ::_thesis: verum
end;

theorem :: PROCAL_1:24
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p <=> q) => (q => p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p <=> q) => (q => p) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p <=> q) => (q => p) in TAUT A
 p <=> q = (p => q) '&' (q => p) by QC_LANG2:def_4;
hence  (p <=> q) => (q => p) in TAUT A by Th21; ::_thesis: verum
end;

theorem Th25: :: PROCAL_1:25
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) in TAUT A
 ( ('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  ((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) in TAUT A by Lm1; ::_thesis: verum
end;

theorem :: PROCAL_1:26
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT A
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  ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT A by LUKASI_1:35; ::_thesis: verum
end;

theorem Th27: :: PROCAL_1:27
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (p 'or' (q 'or' r)) => ((p 'or' q) 'or' r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds (p 'or' (q 'or' r)) => ((p 'or' q) 'or' r) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: (p 'or' (q 'or' r)) => ((p 'or' q) 'or' r) in TAUT A
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  (p 'or' (q 'or' r)) => ((p 'or' q) 'or' r) in TAUT A by Lm1; ::_thesis: verum
end;

theorem Th28: :: PROCAL_1:28
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds p => (q => (p '&' q)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds p => (q => (p '&' q)) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: p => (q => (p '&' q)) in TAUT A
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  p => (q => (p '&' q)) in TAUT A by A5, LUKASI_1:3; ::_thesis: verum
end;

theorem :: PROCAL_1:29
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p => q) => ((q => p) => (p <=> q)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p => q) => ((q => p) => (p <=> q)) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p => q) => ((q => p) => (p <=> q)) in TAUT A
 (p => q) => ((q => p) => ((p => q) '&' (q => p))) in TAUT A by Th28;
hence  (p => q) => ((q => p) => (p <=> q)) in TAUT A by QC_LANG2:def_4; ::_thesis: verum
end;

Lm4:  for A being QC-alphabet
for p, q being Element of CQC-WFF A st p in TAUT A & q in TAUT A holds
p '&' q in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p in TAUT A & q in TAUT A holds
p '&' q in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ( p in TAUT A & q in TAUT A implies p '&' q in TAUT A )
assume that
A1: p in TAUT A and
A2: q in TAUT A ; ::_thesis: p '&' 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  p '&' q in TAUT A by A2, CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:30
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p 'or' q) <=> (q 'or' p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p 'or' q) <=> (q 'or' p) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p 'or' q) <=> (q 'or' p) in TAUT A
set P = p 'or' q;
set Q = q 'or' p;
 ( (p 'or' q) => (q 'or' p) in TAUT A & (q 'or' p) => (p 'or' q) in TAUT A ) by Th8;
then  ((p 'or' q) => (q 'or' p)) '&' ((q 'or' p) => (p 'or' q)) in TAUT A by Lm4;
hence  (p 'or' q) <=> (q 'or' p) in TAUT A by QC_LANG2:def_4; ::_thesis: verum
end;

theorem :: PROCAL_1:31
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p '&' q) => r) => (p => (q => r)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p '&' q) => r) => (p => (q => r)) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ((p '&' q) => r) => (p => (q => r)) in TAUT A
 ( 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  ((p '&' q) => r) => (p => (q => r)) in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;

theorem Th32: :: PROCAL_1:32
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (p => (q => r)) => ((p '&' q) => r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds (p => (q => r)) => ((p '&' q) => r) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: (p => (q => r)) => ((p '&' q) => r) in TAUT A
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  (p => (q => r)) => ((p '&' q) => r) in TAUT A by A2, LUKASI_1:3; ::_thesis: verum
end;

theorem Th33: :: PROCAL_1:33
for A being QC-alphabet
for r, p, q being Element of CQC-WFF A holds (r => p) => ((r => q) => (r => (p '&' q))) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for r, p, q being Element of CQC-WFF A holds (r => p) => ((r => q) => (r => (p '&' q))) in TAUT A
let r, p, q be Element of CQC-WFF A; ::_thesis: (r => p) => ((r => q) => (r => (p '&' q))) in TAUT A
 ( 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  (r => p) => ((r => q) => (r => (p '&' q))) in TAUT A by A1, LUKASI_1:3; ::_thesis: verum
end;

theorem :: PROCAL_1:34
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p 'or' q) => r) => ((p => r) 'or' (q => r)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p 'or' q) => r) => ((p => r) 'or' (q => r)) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ((p 'or' q) => r) => ((p => r) 'or' (q => r)) in TAUT A
 ( 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  ((p 'or' q) => r) => ((p => r) 'or' (q => r)) in TAUT A by Lm1; ::_thesis: verum
end;

theorem Th35: :: PROCAL_1:35
for A being QC-alphabet
for p, r, q being Element of CQC-WFF A holds (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, r, q being Element of CQC-WFF A holds (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A
let p, r, q be Element of CQC-WFF A; ::_thesis: (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A
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: (('not' r) => ('not' p)) => ((('not' r) => ('not' q)) => (('not' r) => (('not' p) '&' ('not' q)))) in TAUT A by Th33;
 (('not' r) => (('not' p) '&' ('not' q))) => (('not' (('not' p) '&' ('not' q))) => r) in TAUT A by LUKASI_1:31;
then  (('not' r) => (('not' p) '&' ('not' q))) => ((p 'or' q) => r) in TAUT A by QC_LANG2:def_3;
then A2: (('not' r) => ('not' q)) => ((('not' r) => (('not' p) '&' ('not' q))) => ((p 'or' q) => r)) in TAUT A by LUKASI_1:13;
 ((('not' r) => ('not' q)) => ((('not' r) => (('not' p) '&' ('not' q))) => ((p 'or' q) => r))) => (((('not' r) => ('not' q)) => (('not' r) => (('not' p) '&' ('not' q)))) => ((('not' r) => ('not' q)) => ((p 'or' q) => r))) in TAUT A by LUKASI_1:11;
then  ((('not' r) => ('not' q)) => (('not' r) => (('not' p) '&' ('not' q)))) => ((('not' r) => ('not' q)) => ((p 'or' q) => r)) in TAUT A by A2, CQC_THE1:46;
then  (('not' r) => ('not' p)) => ((('not' r) => ('not' q)) => ((p 'or' q) => r)) in TAUT A by A1, LUKASI_1:3;
then A3: (('not' r) => ('not' q)) => ((('not' r) => ('not' p)) => ((p 'or' q) => r)) in TAUT A by LUKASI_1:15;
 (q => r) => (('not' r) => ('not' q)) in TAUT A by LUKASI_1:26;
then  (q => r) => ((('not' r) => ('not' p)) => ((p 'or' q) => r)) in TAUT A by A3, LUKASI_1:3;
then A4: (('not' r) => ('not' p)) => ((q => r) => ((p 'or' q) => r)) in TAUT A by LUKASI_1:15;
 (p => r) => (('not' r) => ('not' p)) in TAUT A by LUKASI_1:26;
hence  (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A by A4, LUKASI_1:3; ::_thesis: verum
end;

theorem Th36: :: PROCAL_1:36
for A being QC-alphabet
for p, r, q being Element of CQC-WFF A holds ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, r, q being Element of CQC-WFF A holds ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT A
let p, r, q be Element of CQC-WFF A; ::_thesis: ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT A
set P = p => r;
set Q = q => r;
set R = (p 'or' q) => r;
 ( (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A & ((p => r) => ((q => r) => ((p 'or' q) => r))) => (((p => r) '&' (q => r)) => ((p 'or' q) => r)) in TAUT A ) by Th32, Th35;
hence  ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:37
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p => (q '&' ('not' q))) => ('not' p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p => (q '&' ('not' q))) => ('not' p) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p => (q '&' ('not' q))) => ('not' p) in TAUT A
 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  (p => (q '&' ('not' q))) => ('not' p) in TAUT A by A3, LUKASI_1:3; ::_thesis: verum
end;

theorem :: PROCAL_1:38
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT A
 (('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  ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:39
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT A
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  (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT A by LUKASI_1:35; ::_thesis: verum
end;

theorem Th40: :: PROCAL_1:40
for A being QC-alphabet
for p, r, q being Element of CQC-WFF A holds ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, r, q being Element of CQC-WFF A holds ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A
let p, r, q be Element of CQC-WFF A; ::_thesis: ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A
 ((('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  ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A by Lm1; ::_thesis: verum
end;

Lm5:  for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(r '&' p) => (r '&' q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(r '&' p) => (r '&' q) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A implies (r '&' p) => (r '&' q) in TAUT A )
A1: ('not' (r => ('not' q))) => (r '&' q) in TAUT A by Th16;
assume  p => q in TAUT A ; ::_thesis: (r '&' p) => (r '&' 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  (r '&' p) => (r '&' q) in TAUT A by A1, LUKASI_1:3; ::_thesis: verum
end;

Lm6:  for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(p 'or' r) => (q 'or' r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(p 'or' r) => (q 'or' r) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A implies (p 'or' r) => (q 'or' r) in TAUT A )
assume  p => q in TAUT A ; ::_thesis: (p 'or' r) => (q 'or' r) 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  (p 'or' r) => (q 'or' r) in TAUT A by Lm1; ::_thesis: verum
end;

Lm7:  for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(r 'or' p) => (r 'or' q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(r 'or' p) => (r 'or' q) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A implies (r 'or' p) => (r 'or' q) in TAUT A )
assume  p => q in TAUT A ; ::_thesis: (r 'or' p) => (r 'or' 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  (r 'or' p) => (r 'or' q) in TAUT A by Lm1; ::_thesis: verum
end;

theorem :: PROCAL_1:41
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT A
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  ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT A by A5, LUKASI_1:3; ::_thesis: verum
end;

theorem :: PROCAL_1:42
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p in TAUT A holds
p 'or' q in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p in TAUT A holds
p 'or' q in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ( p in TAUT A implies p 'or' q in TAUT A )
assume A1: p in TAUT A ; ::_thesis: p 'or' q in TAUT A
 p => (p 'or' q) in TAUT A by Th3;
hence  p 'or' q in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:43
for A being QC-alphabet
for q, p being Element of CQC-WFF A st q in TAUT A holds
p 'or' q in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A st q in TAUT A holds
p 'or' q in TAUT A
let q, p be Element of CQC-WFF A; ::_thesis: ( q in TAUT A implies p 'or' q in TAUT A )
assume A1: q in TAUT A ; ::_thesis: p 'or' q in TAUT A
 q => (p 'or' q) in TAUT A by Th4;
hence  p 'or' q in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:44
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds
p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds
p in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ( p '&' q in TAUT A implies p in TAUT A )
assume A1: p '&' q in TAUT A ; ::_thesis: p in TAUT A
 (p '&' q) => p in TAUT A by Th19;
hence  p in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:45
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds
q in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds
q in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ( p '&' q in TAUT A implies q in TAUT A )
assume A1: p '&' q in TAUT A ; ::_thesis: q in TAUT A
 (p '&' q) => q in TAUT A by Th21;
hence  q in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:46
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds
p 'or' q in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds
p 'or' q in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ( p '&' q in TAUT A implies p 'or' q in TAUT A )
assume A1: p '&' q in TAUT A ; ::_thesis: p 'or' q in TAUT A
 (p '&' q) => (p 'or' q) in TAUT A by Th20;
hence  p 'or' q in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:47
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p in TAUT A & q in TAUT A holds
p '&' q in TAUT A by Lm4;

theorem :: PROCAL_1:48
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(p 'or' r) => (q 'or' r) in TAUT A by Lm6;

theorem :: PROCAL_1:49
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(r 'or' p) => (r 'or' q) in TAUT A by Lm7;

theorem :: PROCAL_1:50
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(r '&' p) => (r '&' q) in TAUT A by Lm5;

theorem Th51: :: PROCAL_1:51
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(p '&' r) => (q '&' r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(p '&' r) => (q '&' r) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A implies (p '&' r) => (q '&' r) in TAUT A )
A1: (p => q) => ((q => ('not' r)) => (p => ('not' r))) in TAUT A by LUKASI_1:1;
assume  p => q in TAUT A ; ::_thesis: (p '&' r) => (q '&' r) 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  (p '&' r) => (q '&' r) in TAUT A by A3, LUKASI_1:3; ::_thesis: verum
end;

theorem :: PROCAL_1:52
for A being QC-alphabet
for r, p, q being Element of CQC-WFF A st r => p in TAUT A & r => q in TAUT A holds
r => (p '&' q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for r, p, q being Element of CQC-WFF A st r => p in TAUT A & r => q in TAUT A holds
r => (p '&' q) in TAUT A
let r, p, q be Element of CQC-WFF A; ::_thesis: ( r => p in TAUT A & r => q in TAUT A implies r => (p '&' q) in TAUT A )
assume that
A1: r => p in TAUT A and
A2: r => q in TAUT A ; ::_thesis: r => (p '&' 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  r => (p '&' q) in TAUT A by A2, CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:53
for A being QC-alphabet
for p, r, q being Element of CQC-WFF A st p => r in TAUT A & q => r in TAUT A holds
(p 'or' q) => r in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, r, q being Element of CQC-WFF A st p => r in TAUT A & q => r in TAUT A holds
(p 'or' q) => r in TAUT A
let p, r, q be Element of CQC-WFF A; ::_thesis: ( p => r in TAUT A & q => r in TAUT A implies (p 'or' q) => r in TAUT A )
assume  ( p => r in TAUT A & q => r in TAUT A ) ; ::_thesis: (p 'or' 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  (p 'or' q) => r in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:54
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p 'or' q in TAUT A & 'not' p in TAUT A holds
q in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p 'or' q in TAUT A & 'not' p in TAUT A holds
q in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ( p 'or' q in TAUT A & 'not' p in TAUT A implies q in TAUT A )
assume that
A1: p 'or' q in TAUT A and
A2: 'not' p in TAUT A ; ::_thesis: q 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  q in TAUT A by A2, CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:55
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p 'or' q in TAUT A & 'not' q in TAUT A holds
p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p 'or' q in TAUT A & 'not' q in TAUT A holds
p in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ( p 'or' q in TAUT A & 'not' q in TAUT A implies p in TAUT A )
assume that
A1: p 'or' q in TAUT A and
A2: 'not' q in TAUT A ; ::_thesis: p 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  p in TAUT A by A2, CQC_THE1:46; ::_thesis: verum
end;

theorem :: PROCAL_1:56
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p => q in TAUT A & r => s in TAUT A holds
(p '&' r) => (q '&' s) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p => q in TAUT A & r => s in TAUT A holds
(p '&' r) => (q '&' s) in TAUT A
let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A & r => s in TAUT A implies (p '&' r) => (q '&' s) in TAUT A )
assume  ( p => q in TAUT A & r => s in TAUT A ) ; ::_thesis: (p '&' r) => (q '&' s) in TAUT A
then  ( (p '&' r) => (q '&' r) in TAUT A & (q '&' r) => (q '&' s) in TAUT A ) by Lm5, Th51;
hence  (p '&' r) => (q '&' s) in TAUT A by LUKASI_1:3; ::_thesis: verum
end;

theorem :: PROCAL_1:57
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p => q in TAUT A & r => s in TAUT A holds
(p 'or' r) => (q 'or' s) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p => q in TAUT A & r => s in TAUT A holds
(p 'or' r) => (q 'or' s) in TAUT A
let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A & r => s in TAUT A implies (p 'or' r) => (q 'or' s) in TAUT A )
assume  ( p => q in TAUT A & r => s in TAUT A ) ; ::_thesis: (p 'or' r) => (q 'or' 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  (p 'or' r) => (q 'or' s) in TAUT A by LUKASI_1:3; ::_thesis: verum
end;

theorem :: PROCAL_1:58
for A being QC-alphabet
for p, q being Element of CQC-WFF A st (p '&' ('not' q)) => ('not' p) in TAUT A holds
p => q in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st (p '&' ('not' q)) => ('not' p) in TAUT A holds
p => q in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ( (p '&' ('not' q)) => ('not' p) in TAUT A implies p => q in TAUT A )
A1: 'not' (p '&' ('not' q)) = p => q by QC_LANG2:def_2;
assume  (p '&' ('not' q)) => ('not' p) in TAUT A ; ::_thesis: p => q 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  p => q in TAUT A by A1, LUKASI_1:18; ::_thesis: verum
end;