:: LUKASI_1 semantic presentation

theorem Th1: :: LUKASI_1:1

for b₁, b₂, b₃ being Element of CQC-WFF holds (b₁ => b₂) => ((b₂ => b₃) => (b₁ => b₃)) in TAUT

proof end;

theorem Th2: :: LUKASI_1:2

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => b₂ in TAUT holds
(b₂ => b₃) => (b₁ => b₃) in TAUT

proof end;

theorem Th3: :: LUKASI_1:3

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => b₂ in TAUT & b₂ => b₃ in TAUT holds
b₁ => b₃ in TAUT

proof end;

theorem Th4: :: LUKASI_1:4

for b₁ being Element of CQC-WFF holds b₁ => b₁ in TAUT

proof end;

Lemma5: for b₁, b₂, b₃, b₄ being Element of CQC-WFF holds (((b₁ => b₂) => (b₃ => b₂)) => b₄) => ((b₃ => b₁) => b₄) in TAUT

proof end;

Lemma6: for b₁, b₂, b₃, b₄ being Element of CQC-WFF holds (b₁ => (b₂ => b₃)) => ((b₄ => b₂) => (b₁ => (b₄ => b₃))) in TAUT

proof end;

Lemma7: for b₁, b₂, b₃, b₄ being Element of CQC-WFF holds (b₁ => b₂) => (((b₁ => b₃) => b₄) => ((b₂ => b₃) => b₄)) in TAUT

proof end;

Lemma8: for b₁, b₂, b₃, b₄, b₅ being Element of CQC-WFF holds (b₁ => ((b₂ => b₃) => b₄)) => ((b₂ => b₅) => (b₁ => ((b₅ => b₃) => b₄))) in TAUT

proof end;

Lemma9: for b₁, b₂, b₃ being Element of CQC-WFF holds ((('not' b₁) => b₂) => b₃) => (b₁ => b₃) in TAUT

proof end;

Lemma10: for b₁, b₂, b₃, b₄ being Element of CQC-WFF holds b₁ => (((('not' b₁) => b₂) => b₃) => ((b₄ => b₂) => b₃)) in TAUT

proof end;

Lemma11: for b₁, b₂ being Element of CQC-WFF holds (b₁ => ((('not' b₂) => b₂) => b₂)) => ((('not' b₂) => b₂) => b₂) in TAUT

proof end;

Lemma12: for b₁, b₂ being Element of CQC-WFF holds b₁ => ((('not' b₂) => b₂) => b₂) in TAUT

proof end;

Lemma13: for b₁, b₂, b₃ being Element of CQC-WFF holds (('not' b₁) => b₂) => (b₃ => ((b₂ => b₁) => b₁)) in TAUT

proof end;

Lemma14: for b₁, b₂, b₃, b₄ being Element of CQC-WFF holds ((b₁ => ((b₂ => b₃) => b₃)) => b₄) => ((('not' b₃) => b₂) => b₄) in TAUT

proof end;

Lemma15: for b₁, b₂ being Element of CQC-WFF holds (('not' b₁) => b₂) => ((b₂ => b₁) => b₁) in TAUT

proof end;

Lemma16: for b₁, b₂ being Element of CQC-WFF holds b₁ => ((b₂ => b₁) => b₁) in TAUT

proof end;

theorem Th5: :: LUKASI_1:5

for b₁, b₂ being Element of CQC-WFF holds b₁ => (b₂ => b₁) in TAUT

proof end;

theorem Th6: :: LUKASI_1:6

for b₁, b₂, b₃ being Element of CQC-WFF holds ((b₁ => b₂) => b₃) => (b₂ => b₃) in TAUT

proof end;

theorem Th7: :: LUKASI_1:7

for b₁, b₂ being Element of CQC-WFF holds b₁ => ((b₁ => b₂) => b₂) in TAUT

proof end;

theorem Th8: :: LUKASI_1:8

for b₁, b₂, b₃ being Element of CQC-WFF holds (b₁ => (b₂ => b₃)) => (b₂ => (b₁ => b₃)) in TAUT

proof end;

theorem Th9: :: LUKASI_1:9

for b₁, b₂, b₃ being Element of CQC-WFF holds (b₁ => b₂) => ((b₃ => b₁) => (b₃ => b₂)) in TAUT

proof end;

Lemma22: for b₁, b₂, b₃, b₄ being Element of CQC-WFF holds ((b₁ => (b₂ => b₃)) => b₄) => ((b₂ => (b₁ => b₃)) => b₄) in TAUT

proof end;

Lemma23: for b₁, b₂ being Element of CQC-WFF holds ((b₁ => b₂) => b₁) => b₁ in TAUT

proof end;

Lemma24: for b₁, b₂, b₃, b₄ being Element of CQC-WFF holds ((b₁ => b₂) => b₃) => ((b₁ => b₄) => ((b₄ => b₂) => b₃)) in TAUT

proof end;

Lemma25: for b₁, b₂, b₃ being Element of CQC-WFF holds ((b₁ => b₂) => b₃) => ((b₃ => b₁) => b₁) in TAUT

proof end;

Lemma26: for b₁, b₂, b₃, b₄ being Element of CQC-WFF holds (((b₁ => b₂) => b₂) => b₃) => (((b₂ => b₄) => b₁) => b₃) in TAUT

proof end;

Lemma27: for b₁, b₂, b₃ being Element of CQC-WFF holds ((b₁ => b₂) => b₃) => ((b₁ => b₃) => b₃) in TAUT

proof end;

theorem Th10: :: LUKASI_1:10

for b₁, b₂ being Element of CQC-WFF holds (b₁ => (b₁ => b₂)) => (b₁ => b₂) in TAUT

proof end;

Lemma29: for b₁, b₂, b₃, b₄ being Element of CQC-WFF holds (b₁ => b₂) => (((b₁ => b₃) => b₄) => ((b₂ => b₄) => b₄)) in TAUT

proof end;

Lemma30: for b₁, b₂, b₃, b₄ being Element of CQC-WFF holds ((b₁ => b₂) => b₃) => ((b₁ => b₄) => ((b₄ => b₃) => b₃)) in TAUT

proof end;

Lemma31: for b₁, b₂, b₃, b₄ being Element of CQC-WFF holds (b₁ => b₂) => ((b₂ => (b₃ => (b₁ => b₄))) => (b₃ => (b₁ => b₄))) in TAUT

proof end;

Lemma32: for b₁, b₂, b₃, b₄ being Element of CQC-WFF holds (b₁ => (b₂ => (b₃ => b₄))) => ((b₃ => b₁) => (b₂ => (b₃ => b₄))) in TAUT

proof end;

theorem Th11: :: LUKASI_1:11

for b₁, b₂, b₃ being Element of CQC-WFF holds (b₁ => (b₂ => b₃)) => ((b₁ => b₂) => (b₁ => b₃)) in TAUT

proof end;

theorem Th12: :: LUKASI_1:12

for b₁ being Element of CQC-WFF holds ('not' VERUM ) => b₁ in TAUT

proof end;

theorem Th13: :: LUKASI_1:13

for b₁, b₂ being Element of CQC-WFF st b₁ in TAUT holds
b₂ => b₁ in TAUT

proof end;

theorem Th14: :: LUKASI_1:14

for b₁, b₂ being Element of CQC-WFF st b₁ in TAUT holds
(b₁ => b₂) => b₂ in TAUT

proof end;

theorem Th15: :: LUKASI_1:15

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => (b₂ => b₃) in TAUT holds
b₂ => (b₁ => b₃) in TAUT

proof end;

theorem Th16: :: LUKASI_1:16

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => (b₂ => b₃) in TAUT & b₂ in TAUT holds
b₁ => b₃ in TAUT

proof end;

theorem Th17: :: LUKASI_1:17

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => (b₂ => b₃) in TAUT & b₂ in TAUT & b₁ in TAUT holds
b₃ in TAUT

proof end;

theorem Th18: :: LUKASI_1:18

for b₁, b₂ being Element of CQC-WFF st b₁ => (b₁ => b₂) in TAUT holds
b₁ => b₂ in TAUT

proof end;

theorem Th19: :: LUKASI_1:19

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => (b₂ => b₃) in TAUT holds
(b₁ => b₂) => (b₁ => b₃) in TAUT

proof end;

theorem Th20: :: LUKASI_1:20

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => (b₂ => b₃) in TAUT & b₁ => b₂ in TAUT holds
b₁ => b₃ in TAUT

proof end;

theorem Th21: :: LUKASI_1:21

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ => (b₂ => b₃) in TAUT & b₁ => b₂ in TAUT & b₁ in TAUT holds
b₃ in TAUT

proof end;

theorem Th22: :: LUKASI_1:22

for b₁, b₂, b₃, b₄ being Element of CQC-WFF st b₁ => (b₂ => b₃) in TAUT & b₁ => (b₃ => b₄) in TAUT holds
b₁ => (b₂ => b₄) in TAUT

proof end;

theorem Th23: :: LUKASI_1:23

for b₁ being Element of CQC-WFF holds b₁ => VERUM in TAUT by Th13, CQC_THE1:77;

Lemma41: for b₁ being Element of CQC-WFF holds ('not' b₁) => (b₁ => ('not' VERUM )) in TAUT

proof end;

Lemma42: for b₁ being Element of CQC-WFF holds (('not' b₁) => ('not' VERUM )) => b₁ in TAUT

proof end;

theorem Th24: :: LUKASI_1:24

for b₁, b₂ being Element of CQC-WFF holds (('not' b₁) => ('not' b₂)) => (b₂ => b₁) in TAUT

proof end;

theorem Th25: :: LUKASI_1:25

for b₁ being Element of CQC-WFF holds ('not' ('not' b₁)) => b₁ in TAUT

proof end;

E45: now

let c₁ be Element of CQC-WFF ;
('not' ('not' c₁)) => c₁ in TAUT by Th25;
then E46: (c₁ => ('not' VERUM )) => (('not' ('not' c₁)) => ('not' VERUM )) in TAUT by Th2;
(('not' ('not' c₁)) => ('not' VERUM )) => ('not' c₁) in TAUT by Lemma42;
hence (c₁ => ('not' VERUM )) => ('not' c₁) in TAUT by E46, Th3;

end;

theorem Th26: :: LUKASI_1:26

for b₁, b₂ being Element of CQC-WFF holds (b₁ => b₂) => (('not' b₂) => ('not' b₁)) in TAUT

proof end;

theorem Th27: :: LUKASI_1:27

for b₁ being Element of CQC-WFF holds b₁ => ('not' ('not' b₁)) in TAUT

proof end;

theorem Th28: :: LUKASI_1:28

for b₁, b₂ being Element of CQC-WFF holds
( (('not' ('not' b₁)) => b₂) => (b₁ => b₂) in TAUT & (b₁ => b₂) => (('not' ('not' b₁)) => b₂) in TAUT )

proof end;

theorem Th29: :: LUKASI_1:29

for b₁, b₂ being Element of CQC-WFF holds
( (b₁ => ('not' ('not' b₂))) => (b₁ => b₂) in TAUT & (b₁ => b₂) => (b₁ => ('not' ('not' b₂))) in TAUT )

proof end;

theorem Th30: :: LUKASI_1:30

for b₁, b₂ being Element of CQC-WFF holds (b₁ => ('not' b₂)) => (b₂ => ('not' b₁)) in TAUT

proof end;

theorem Th31: :: LUKASI_1:31

for b₁, b₂ being Element of CQC-WFF holds (('not' b₁) => b₂) => (('not' b₂) => b₁) in TAUT

proof end;

theorem Th32: :: LUKASI_1:32

for b₁ being Element of CQC-WFF holds (b₁ => ('not' b₁)) => ('not' b₁) in TAUT

proof end;

theorem Th33: :: LUKASI_1:33

for b₁, b₂ being Element of CQC-WFF holds ('not' b₁) => (b₁ => b₂) in TAUT

proof end;

theorem Th34: :: LUKASI_1:34

for b₁, b₂ being Element of CQC-WFF holds
( b₁ => b₂ in TAUT iff ('not' b₂) => ('not' b₁) in TAUT )

proof end;

theorem Th35: :: LUKASI_1:35

for b₁, b₂ being Element of CQC-WFF st ('not' b₁) => ('not' b₂) in TAUT holds
b₂ => b₁ in TAUT by Th34;

theorem Th36: :: LUKASI_1:36

for b₁ being Element of CQC-WFF holds
( b₁ in TAUT iff 'not' ('not' b₁) in TAUT )

proof end;

theorem Th37: :: LUKASI_1:37

for b₁, b₂ being Element of CQC-WFF holds
( b₁ => b₂ in TAUT iff b₁ => ('not' ('not' b₂)) in TAUT )

proof end;

theorem Th38: :: LUKASI_1:38

for b₁, b₂ being Element of CQC-WFF holds
( b₁ => b₂ in TAUT iff ('not' ('not' b₁)) => b₂ in TAUT )

proof end;

theorem Th39: :: LUKASI_1:39

for b₁, b₂ being Element of CQC-WFF st b₁ => ('not' b₂) in TAUT holds
b₂ => ('not' b₁) in TAUT

proof end;

theorem Th40: :: LUKASI_1:40

for b₁, b₂ being Element of CQC-WFF st ('not' b₁) => b₂ in TAUT holds
('not' b₂) => b₁ in TAUT

proof end;

theorem Th41: :: LUKASI_1:41

for b₁, b₂, b₃ being Element of CQC-WFF holds |- (b₁ => b₂) => ((b₂ => b₃) => (b₁ => b₃))

proof end;

theorem Th42: :: LUKASI_1:42

for b₁, b₂, b₃ being Element of CQC-WFF st |- b₁ => b₂ holds
|- (b₂ => b₃) => (b₁ => b₃)

proof end;

theorem Th43: :: LUKASI_1:43

for b₁, b₂, b₃ being Element of CQC-WFF st |- b₁ => b₂ & |- b₂ => b₃ holds
|- b₁ => b₃

proof end;

theorem Th44: :: LUKASI_1:44

for b₁ being Element of CQC-WFF holds |- b₁ => b₁

proof end;

theorem Th45: :: LUKASI_1:45

for b₁, b₂ being Element of CQC-WFF holds |- b₁ => (b₂ => b₁)

proof end;

theorem Th46: :: LUKASI_1:46

for b₁, b₂ being Element of CQC-WFF st |- b₁ holds
|- b₂ => b₁

proof end;

theorem Th47: :: LUKASI_1:47

for b₁, b₂, b₃ being Element of CQC-WFF holds |- (b₁ => (b₂ => b₃)) => (b₂ => (b₁ => b₃))

proof end;

theorem Th48: :: LUKASI_1:48

for b₁, b₂, b₃ being Element of CQC-WFF st |- b₁ => (b₂ => b₃) holds
|- b₂ => (b₁ => b₃)

proof end;

theorem Th49: :: LUKASI_1:49

for b₁, b₂, b₃ being Element of CQC-WFF st |- b₁ => (b₂ => b₃) & |- b₂ holds
|- b₁ => b₃

proof end;

theorem Th50: :: LUKASI_1:50

for b₁ being Element of CQC-WFF holds
( |- b₁ => VERUM & |- ('not' VERUM ) => b₁ )

proof end;

theorem Th51: :: LUKASI_1:51

for b₁, b₂ being Element of CQC-WFF holds |- b₁ => ((b₁ => b₂) => b₂)

proof end;

theorem Th52: :: LUKASI_1:52

for b₁, b₂ being Element of CQC-WFF holds |- (b₁ => (b₁ => b₂)) => (b₁ => b₂)

proof end;

theorem Th53: :: LUKASI_1:53

for b₁, b₂ being Element of CQC-WFF st |- b₁ => (b₁ => b₂) holds
|- b₁ => b₂

proof end;

theorem Th54: :: LUKASI_1:54

for b₁, b₂, b₃ being Element of CQC-WFF holds |- (b₁ => (b₂ => b₃)) => ((b₁ => b₂) => (b₁ => b₃))

proof end;

theorem Th55: :: LUKASI_1:55

for b₁, b₂, b₃ being Element of CQC-WFF st |- b₁ => (b₂ => b₃) holds
|- (b₁ => b₂) => (b₁ => b₃)

proof end;

theorem Th56: :: LUKASI_1:56

for b₁, b₂, b₃ being Element of CQC-WFF st |- b₁ => (b₂ => b₃) & |- b₁ => b₂ holds
|- b₁ => b₃

proof end;

theorem Th57: :: LUKASI_1:57

for b₁, b₂, b₃ being Element of CQC-WFF holds |- ((b₁ => b₂) => b₃) => (b₂ => b₃)

proof end;

theorem Th58: :: LUKASI_1:58

for b₁, b₂, b₃ being Element of CQC-WFF st |- (b₁ => b₂) => b₃ holds
|- b₂ => b₃

proof end;

theorem Th59: :: LUKASI_1:59

for b₁, b₂, b₃ being Element of CQC-WFF holds |- (b₁ => b₂) => ((b₃ => b₁) => (b₃ => b₂))

proof end;

theorem Th60: :: LUKASI_1:60

for b₁, b₂, b₃ being Element of CQC-WFF st |- b₁ => b₂ holds
|- (b₃ => b₁) => (b₃ => b₂)

proof end;

theorem Th61: :: LUKASI_1:61

for b₁, b₂ being Element of CQC-WFF holds |- (b₁ => b₂) => (('not' b₂) => ('not' b₁))

proof end;

theorem Th62: :: LUKASI_1:62

for b₁, b₂ being Element of CQC-WFF holds |- (('not' b₁) => ('not' b₂)) => (b₂ => b₁)

proof end;

theorem Th63: :: LUKASI_1:63

for b₁, b₂ being Element of CQC-WFF holds
( |- ('not' b₁) => ('not' b₂) iff |- b₂ => b₁ )

proof end;

theorem Th64: :: LUKASI_1:64

for b₁ being Element of CQC-WFF holds |- b₁ => ('not' ('not' b₁))

proof end;

theorem Th65: :: LUKASI_1:65

for b₁ being Element of CQC-WFF holds |- ('not' ('not' b₁)) => b₁

proof end;

theorem Th66: :: LUKASI_1:66

for b₁ being Element of CQC-WFF holds
( |- 'not' ('not' b₁) iff |- b₁ )

proof end;

theorem Th67: :: LUKASI_1:67

for b₁, b₂ being Element of CQC-WFF holds |- (('not' ('not' b₁)) => b₂) => (b₁ => b₂)

proof end;

theorem Th68: :: LUKASI_1:68

for b₁, b₂ being Element of CQC-WFF holds
( |- ('not' ('not' b₁)) => b₂ iff |- b₁ => b₂ )

proof end;

theorem Th69: :: LUKASI_1:69

for b₁, b₂ being Element of CQC-WFF holds |- (b₁ => ('not' ('not' b₂))) => (b₁ => b₂)

proof end;

theorem Th70: :: LUKASI_1:70

for b₁, b₂ being Element of CQC-WFF holds
( |- b₁ => ('not' ('not' b₂)) iff |- b₁ => b₂ )

proof end;

theorem Th71: :: LUKASI_1:71

for b₁, b₂ being Element of CQC-WFF holds |- (b₁ => ('not' b₂)) => (b₂ => ('not' b₁))

proof end;

theorem Th72: :: LUKASI_1:72

for b₁, b₂ being Element of CQC-WFF st |- b₁ => ('not' b₂) holds
|- b₂ => ('not' b₁)

proof end;

theorem Th73: :: LUKASI_1:73

for b₁, b₂ being Element of CQC-WFF holds |- (('not' b₁) => b₂) => (('not' b₂) => b₁)

proof end;

theorem Th74: :: LUKASI_1:74

for b₁, b₂ being Element of CQC-WFF st |- ('not' b₁) => b₂ holds
|- ('not' b₂) => b₁

proof end;

theorem Th75: :: LUKASI_1:75

for b₁, b₂, b₃ being Element of CQC-WFF
for b₄ being Subset of CQC-WFF st b₄ |- b₁ => b₂ holds
b₄ |- (b₂ => b₃) => (b₁ => b₃)

proof end;

theorem Th76: :: LUKASI_1:76

for b₁, b₂, b₃ being Element of CQC-WFF
for b₄ being Subset of CQC-WFF st b₄ |- b₁ => b₂ & b₄ |- b₂ => b₃ holds
b₄ |- b₁ => b₃

proof end;

theorem Th77: :: LUKASI_1:77

for b₁ being Element of CQC-WFF
for b₂ being Subset of CQC-WFF holds b₂ |- b₁ => b₁

proof end;

theorem Th78: :: LUKASI_1:78

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF st b₃ |- b₁ holds
b₃ |- b₂ => b₁

proof end;

theorem Th79: :: LUKASI_1:79

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF st b₃ |- b₁ holds
b₃ |- (b₁ => b₂) => b₂

proof end;

theorem Th80: :: LUKASI_1:80

for b₁, b₂, b₃ being Element of CQC-WFF
for b₄ being Subset of CQC-WFF st b₄ |- b₁ => (b₂ => b₃) holds
b₄ |- b₂ => (b₁ => b₃)

proof end;

theorem Th81: :: LUKASI_1:81

for b₁, b₂, b₃ being Element of CQC-WFF
for b₄ being Subset of CQC-WFF st b₄ |- b₁ => (b₂ => b₃) & b₄ |- b₂ holds
b₄ |- b₁ => b₃

proof end;

theorem Th82: :: LUKASI_1:82

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF st b₃ |- b₁ => (b₁ => b₂) holds
b₃ |- b₁ => b₂

proof end;

theorem Th83: :: LUKASI_1:83

for b₁, b₂, b₃ being Element of CQC-WFF
for b₄ being Subset of CQC-WFF st b₄ |- (b₁ => b₂) => b₃ holds
b₄ |- b₂ => b₃

proof end;

theorem Th84: :: LUKASI_1:84

for b₁, b₂, b₃ being Element of CQC-WFF
for b₄ being Subset of CQC-WFF st b₄ |- b₁ => (b₂ => b₃) holds
b₄ |- (b₁ => b₂) => (b₁ => b₃)

proof end;

theorem Th85: :: LUKASI_1:85

for b₁, b₂, b₃ being Element of CQC-WFF
for b₄ being Subset of CQC-WFF st b₄ |- b₁ => (b₂ => b₃) & b₄ |- b₁ => b₂ holds
b₄ |- b₁ => b₃

proof end;

theorem Th86: :: LUKASI_1:86

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF holds
( b₃ |- ('not' b₁) => ('not' b₂) iff b₃ |- b₂ => b₁ )

proof end;

theorem Th87: :: LUKASI_1:87

for b₁ being Element of CQC-WFF
for b₂ being Subset of CQC-WFF holds
( b₂ |- 'not' ('not' b₁) iff b₂ |- b₁ )

proof end;

theorem Th88: :: LUKASI_1:88

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF holds
( b₃ |- b₁ => ('not' ('not' b₂)) iff b₃ |- b₁ => b₂ )

proof end;

theorem Th89: :: LUKASI_1:89

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF holds
( b₃ |- ('not' ('not' b₁)) => b₂ iff b₃ |- b₁ => b₂ )

proof end;

theorem Th90: :: LUKASI_1:90

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF st b₃ |- b₁ => ('not' b₂) holds
b₃ |- b₂ => ('not' b₁)

proof end;

theorem Th91: :: LUKASI_1:91

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF st b₃ |- ('not' b₁) => b₂ holds
b₃ |- ('not' b₂) => b₁

proof end;

theorem Th92: :: LUKASI_1:92

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF st b₃ |- b₁ => ('not' b₂) & b₃ |- b₂ holds
b₃ |- 'not' b₁

proof end;

theorem Th93: :: LUKASI_1:93

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF st b₃ |- ('not' b₁) => b₂ & b₃ |- 'not' b₂ holds
b₃ |- b₁

proof end;