:: CQC_THE2 semantic presentation

theorem Th1: :: CQC_THE2:1

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

proof end;

theorem Th2: :: CQC_THE2:2

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

proof end;

theorem Th3: :: CQC_THE2:3

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

proof end;

theorem Th4: :: CQC_THE2:4

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

proof end;

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

proof end;

Lemma6: for b₁, b₂ being Element of CQC-WFF st |- b₁ '&' b₂ holds
( |- b₁ & |- b₂ )

proof end;

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

proof end;

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

proof end;

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

proof end;

Lemma10: for b₁, b₂ being Element of CQC-WFF holds
( |- b₁ => (b₁ 'or' b₂) & |- b₁ => (b₂ 'or' b₁) )

proof end;

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

proof end;

Lemma12: for b₁, b₂ being Element of CQC-WFF st |- b₁ & |- b₂ holds
|- b₁ '&' b₂

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

Lemma18: for b₁, b₂ being Element of CQC-WFF holds
( ( |- b₁ => b₂ & |- b₂ => b₁ ) iff |- b₁ <=> b₂ )

proof end;

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

proof end;

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

proof end;

theorem Th5: :: CQC_THE2:5

for b₁ being QC-formula
for b₂, b₃ being bound_QC-variable holds
( b₂ in still_not-bound_in (All b₃,b₁) iff ( b₂ in still_not-bound_in b₁ & b₂ <> b₃ ) )

proof end;

theorem Th6: :: CQC_THE2:6

for b₁ being QC-formula
for b₂, b₃ being bound_QC-variable holds
( b₂ in still_not-bound_in (Ex b₃,b₁) iff ( b₂ in still_not-bound_in b₁ & b₂ <> b₃ ) )

proof end;

theorem Th7: :: CQC_THE2:7

for b₁, b₂ being QC-formula
for b₃ being bound_QC-variable holds
( b₃ in still_not-bound_in (b₁ => b₂) iff ( b₃ in still_not-bound_in b₁ or b₃ in still_not-bound_in b₂ ) )

proof end;

theorem Th8: :: CQC_THE2:8

canceled;

theorem Th9: :: CQC_THE2:9

for b₁, b₂ being QC-formula
for b₃ being bound_QC-variable holds
( b₃ in still_not-bound_in (b₁ '&' b₂) iff ( b₃ in still_not-bound_in b₁ or b₃ in still_not-bound_in b₂ ) )

proof end;

theorem Th10: :: CQC_THE2:10

for b₁, b₂ being QC-formula
for b₃ being bound_QC-variable holds
( b₃ in still_not-bound_in (b₁ 'or' b₂) iff ( b₃ in still_not-bound_in b₁ or b₃ in still_not-bound_in b₂ ) )

proof end;

theorem Th11: :: CQC_THE2:11

for b₁ being QC-formula
for b₂, b₃ being bound_QC-variable holds
( not b₂ in still_not-bound_in (All b₂,b₃,b₁) & not b₃ in still_not-bound_in (All b₂,b₃,b₁) )

proof end;

theorem Th12: :: CQC_THE2:12

for b₁ being QC-formula
for b₂, b₃ being bound_QC-variable holds
( not b₂ in still_not-bound_in (Ex b₂,b₃,b₁) & not b₃ in still_not-bound_in (Ex b₂,b₃,b₁) )

proof end;

theorem Th13: :: CQC_THE2:13

canceled;

theorem Th14: :: CQC_THE2:14

for b₁, b₂ being QC-formula
for b₃ being bound_QC-variable holds (b₁ => b₂) . b₃ = (b₁ . b₃) => (b₂ . b₃)

proof end;

theorem Th15: :: CQC_THE2:15

for b₁, b₂ being QC-formula
for b₃ being bound_QC-variable holds (b₁ 'or' b₂) . b₃ = (b₁ . b₃) 'or' (b₂ . b₃)

proof end;

theorem Th16: :: CQC_THE2:16

canceled;

theorem Th17: :: CQC_THE2:17

for b₁ being Element of CQC-WFF
for b₂, b₃ being bound_QC-variable st b₂ <> b₃ holds
(Ex b₂,b₁) . b₃ = Ex b₂,(b₁ . b₃)

proof end;

theorem Th18: :: CQC_THE2:18

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

proof end;

theorem Th19: :: CQC_THE2:19

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable st |- b₁ holds
|- Ex b₂,b₁

proof end;

theorem Th20: :: CQC_THE2:20

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

proof end;

theorem Th21: :: CQC_THE2:21

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

proof end;

theorem Th22: :: CQC_THE2:22

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st |- b₁ => b₂ & not b₃ in still_not-bound_in b₂ holds
|- (Ex b₃,b₁) => b₂

proof end;

theorem Th23: :: CQC_THE2:23

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable st not b₂ in still_not-bound_in b₁ holds
|- (Ex b₂,b₁) => b₁

proof end;

theorem Th24: :: CQC_THE2:24

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable st not b₂ in still_not-bound_in b₁ & |- Ex b₂,b₁ holds
|- b₁

proof end;

theorem Th25: :: CQC_THE2:25

for b₁, b₂ being Element of CQC-WFF
for b₃ being QC-formula
for b₄, b₅ being bound_QC-variable st b₁ = b₃ . b₄ & b₂ = b₃ . b₅ & not b₅ in still_not-bound_in b₃ holds
|- b₁ => (Ex b₅,b₂)

proof end;

theorem Th26: :: CQC_THE2:26

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable st |- b₁ holds
|- All b₂,b₁

proof end;

theorem Th27: :: CQC_THE2:27

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable st not b₂ in still_not-bound_in b₁ holds
|- b₁ => (All b₂,b₁)

proof end;

theorem Th28: :: CQC_THE2:28

for b₁, b₂ being Element of CQC-WFF
for b₃ being QC-formula
for b₄, b₅ being bound_QC-variable st b₁ = b₃ . b₄ & b₂ = b₃ . b₅ & not b₄ in still_not-bound_in b₃ holds
|- (All b₄,b₁) => b₂

proof end;

theorem Th29: :: CQC_THE2:29

for b₁ being Element of CQC-WFF
for b₂, b₃ being bound_QC-variable st not b₂ in still_not-bound_in b₁ holds
|- (All b₃,b₁) => (All b₂,b₁)

proof end;

theorem Th30: :: CQC_THE2:30

for b₁, b₂ being Element of CQC-WFF
for b₃ being QC-formula
for b₄, b₅ being bound_QC-variable st b₁ = b₃ . b₄ & b₂ = b₃ . b₅ & not b₄ in still_not-bound_in b₃ & not b₅ in still_not-bound_in b₁ holds
|- (All b₄,b₁) => (All b₅,b₂)

proof end;

theorem Th31: :: CQC_THE2:31

for b₁ being Element of CQC-WFF
for b₂, b₃ being bound_QC-variable st not b₂ in still_not-bound_in b₁ holds
|- (Ex b₂,b₁) => (Ex b₃,b₁)

proof end;

theorem Th32: :: CQC_THE2:32

for b₁, b₂ being Element of CQC-WFF
for b₃ being QC-formula
for b₄, b₅ being bound_QC-variable st b₁ = b₃ . b₄ & b₂ = b₃ . b₅ & not b₄ in still_not-bound_in b₂ & not b₅ in still_not-bound_in b₃ holds
|- (Ex b₄,b₁) => (Ex b₅,b₂)

proof end;

theorem Th33: :: CQC_THE2:33

canceled;

theorem Th34: :: CQC_THE2:34

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

proof end;

theorem Th35: :: CQC_THE2:35

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

proof end;

theorem Th36: :: CQC_THE2:36

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

proof end;

theorem Th37: :: CQC_THE2:37

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

proof end;

theorem Th38: :: CQC_THE2:38

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

proof end;

theorem Th39: :: CQC_THE2:39

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

proof end;

theorem Th40: :: CQC_THE2:40

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds
( |- (All b₃,(b₁ '&' b₂)) => ((All b₃,b₁) '&' (All b₃,b₂)) & |- ((All b₃,b₁) '&' (All b₃,b₂)) => (All b₃,(b₁ '&' b₂)) )

proof end;

theorem Th41: :: CQC_THE2:41

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds |- (All b₃,(b₁ '&' b₂)) <=> ((All b₃,b₁) '&' (All b₃,b₂))

proof end;

theorem Th42: :: CQC_THE2:42

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds
( |- All b₃,(b₁ '&' b₂) iff |- (All b₃,b₁) '&' (All b₃,b₂) )

proof end;

theorem Th43: :: CQC_THE2:43

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds |- ((All b₃,b₁) 'or' (All b₃,b₂)) => (All b₃,(b₁ 'or' b₂))

proof end;

theorem Th44: :: CQC_THE2:44

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds
( |- (Ex b₃,(b₁ 'or' b₂)) => ((Ex b₃,b₁) 'or' (Ex b₃,b₂)) & |- ((Ex b₃,b₁) 'or' (Ex b₃,b₂)) => (Ex b₃,(b₁ 'or' b₂)) )

proof end;

theorem Th45: :: CQC_THE2:45

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds |- (Ex b₃,(b₁ 'or' b₂)) <=> ((Ex b₃,b₁) 'or' (Ex b₃,b₂))

proof end;

theorem Th46: :: CQC_THE2:46

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds
( |- Ex b₃,(b₁ 'or' b₂) iff |- (Ex b₃,b₁) 'or' (Ex b₃,b₂) )

proof end;

theorem Th47: :: CQC_THE2:47

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds |- (Ex b₃,(b₁ '&' b₂)) => ((Ex b₃,b₁) '&' (Ex b₃,b₂))

proof end;

theorem Th48: :: CQC_THE2:48

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st |- Ex b₃,(b₁ '&' b₂) holds
|- (Ex b₃,b₁) '&' (Ex b₃,b₂)

proof end;

theorem Th49: :: CQC_THE2:49

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

proof end;

theorem Th50: :: CQC_THE2:50

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

proof end;

theorem Th51: :: CQC_THE2:51

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

proof end;

theorem Th52: :: CQC_THE2:52

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

proof end;

theorem Th53: :: CQC_THE2:53

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable holds
( |- ('not' (Ex b₂,('not' b₁))) => (All b₂,b₁) & |- (All b₂,b₁) => ('not' (Ex b₂,('not' b₁))) )

proof end;

theorem Th54: :: CQC_THE2:54

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable holds |- ('not' (Ex b₂,('not' b₁))) <=> (All b₂,b₁)

proof end;

theorem Th55: :: CQC_THE2:55

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable holds
( |- ('not' (All b₂,b₁)) => (Ex b₂,('not' b₁)) & |- (Ex b₂,('not' b₁)) => ('not' (All b₂,b₁)) )

proof end;

theorem Th56: :: CQC_THE2:56

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable holds |- ('not' (All b₂,b₁)) <=> (Ex b₂,('not' b₁))

proof end;

theorem Th57: :: CQC_THE2:57

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable holds
( |- ('not' (Ex b₂,b₁)) => (All b₂,('not' b₁)) & |- (All b₂,('not' b₁)) => ('not' (Ex b₂,b₁)) )

proof end;

theorem Th58: :: CQC_THE2:58

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable holds |- (All b₂,('not' b₁)) <=> ('not' (Ex b₂,b₁))

proof end;

theorem Th59: :: CQC_THE2:59

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

proof end;

theorem Th60: :: CQC_THE2:60

for b₁, b₂ being Element of CQC-WFF
for b₃ being QC-formula
for b₄, b₅ being bound_QC-variable st b₁ = b₃ . b₄ & b₂ = b₃ . b₅ & not b₅ in still_not-bound_in b₃ holds
|- (All b₄,(All b₅,b₂)) => (All b₄,b₁)

proof end;

theorem Th61: :: CQC_THE2:61

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

proof end;

theorem Th62: :: CQC_THE2:62

for b₁, b₂ being Element of CQC-WFF
for b₃ being QC-formula
for b₄, b₅ being bound_QC-variable st b₁ = b₃ . b₄ & b₂ = b₃ . b₅ & not b₅ in still_not-bound_in b₃ holds
|- (Ex b₄,b₁) => (Ex b₄,b₅,b₂)

proof end;

theorem Th63: :: CQC_THE2:63

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

proof end;

theorem Th64: :: CQC_THE2:64

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

proof end;

theorem Th65: :: CQC_THE2:65

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds
( |- (Ex b₃,(b₁ => b₂)) => ((All b₃,b₁) => (Ex b₃,b₂)) & |- ((All b₃,b₁) => (Ex b₃,b₂)) => (Ex b₃,(b₁ => b₂)) )

proof end;

theorem Th66: :: CQC_THE2:66

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds |- (Ex b₃,(b₁ => b₂)) <=> ((All b₃,b₁) => (Ex b₃,b₂))

proof end;

theorem Th67: :: CQC_THE2:67

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds
( |- Ex b₃,(b₁ => b₂) iff |- (All b₃,b₁) => (Ex b₃,b₂) )

proof end;

theorem Th68: :: CQC_THE2:68

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds |- (All b₃,(b₁ '&' b₂)) => (b₁ '&' (All b₃,b₂))

proof end;

theorem Th69: :: CQC_THE2:69

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds |- (All b₃,(b₁ '&' b₂)) => ((All b₃,b₁) '&' b₂)

proof end;

theorem Th70: :: CQC_THE2:70

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
|- (b₁ '&' (All b₃,b₂)) => (All b₃,(b₁ '&' b₂))

proof end;

theorem Th71: :: CQC_THE2:71

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ & |- b₁ '&' (All b₃,b₂) holds
|- All b₃,(b₁ '&' b₂)

proof end;

theorem Th72: :: CQC_THE2:72

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
( |- (b₁ 'or' (All b₃,b₂)) => (All b₃,(b₁ 'or' b₂)) & |- (All b₃,(b₁ 'or' b₂)) => (b₁ 'or' (All b₃,b₂)) )

proof end;

theorem Th73: :: CQC_THE2:73

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
|- (b₁ 'or' (All b₃,b₂)) <=> (All b₃,(b₁ 'or' b₂))

proof end;

theorem Th74: :: CQC_THE2:74

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
( |- b₁ 'or' (All b₃,b₂) iff |- All b₃,(b₁ 'or' b₂) )

proof end;

theorem Th75: :: CQC_THE2:75

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
( |- (b₁ '&' (Ex b₃,b₂)) => (Ex b₃,(b₁ '&' b₂)) & |- (Ex b₃,(b₁ '&' b₂)) => (b₁ '&' (Ex b₃,b₂)) )

proof end;

theorem Th76: :: CQC_THE2:76

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
|- (b₁ '&' (Ex b₃,b₂)) <=> (Ex b₃,(b₁ '&' b₂))

proof end;

theorem Th77: :: CQC_THE2:77

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
( |- b₁ '&' (Ex b₃,b₂) iff |- Ex b₃,(b₁ '&' b₂) )

proof end;

Lemma60: for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
|- (All b₃,(b₁ => b₂)) => (b₁ => (All b₃,b₂))

proof end;

theorem Th78: :: CQC_THE2:78

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
( |- (All b₃,(b₁ => b₂)) => (b₁ => (All b₃,b₂)) & |- (b₁ => (All b₃,b₂)) => (All b₃,(b₁ => b₂)) )

proof end;

theorem Th79: :: CQC_THE2:79

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
|- (b₁ => (All b₃,b₂)) <=> (All b₃,(b₁ => b₂))

proof end;

theorem Th80: :: CQC_THE2:80

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
( |- All b₃,(b₁ => b₂) iff |- b₁ => (All b₃,b₂) )

proof end;

theorem Th81: :: CQC_THE2:81

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
|- (Ex b₃,(b₂ => b₁)) => ((All b₃,b₂) => b₁)

proof end;

theorem Th82: :: CQC_THE2:82

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

proof end;

theorem Th83: :: CQC_THE2:83

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
( |- (All b₃,b₂) => b₁ iff |- Ex b₃,(b₂ => b₁) )

proof end;

theorem Th84: :: CQC_THE2:84

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
( |- ((Ex b₃,b₂) => b₁) => (All b₃,(b₂ => b₁)) & |- (All b₃,(b₂ => b₁)) => ((Ex b₃,b₂) => b₁) )

proof end;

theorem Th85: :: CQC_THE2:85

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
|- ((Ex b₃,b₂) => b₁) <=> (All b₃,(b₂ => b₁))

proof end;

theorem Th86: :: CQC_THE2:86

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
( |- (Ex b₃,b₂) => b₁ iff |- All b₃,(b₂ => b₁) )

proof end;

theorem Th87: :: CQC_THE2:87

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
|- (Ex b₃,(b₁ => b₂)) => (b₁ => (Ex b₃,b₂))

proof end;

theorem Th88: :: CQC_THE2:88

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

proof end;

theorem Th89: :: CQC_THE2:89

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
|- (b₁ => (Ex b₃,b₂)) <=> (Ex b₃,(b₁ => b₂))

proof end;

theorem Th90: :: CQC_THE2:90

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st not b₃ in still_not-bound_in b₁ holds
( |- b₁ => (Ex b₃,b₂) iff |- Ex b₃,(b₁ => b₂) )

proof end;

theorem Th91: :: CQC_THE2:91

for b₁ being Element of CQC-WFF holds {b₁} |- b₁

proof end;

theorem Th92: :: CQC_THE2:92

for b₁, b₂ being Element of CQC-WFF holds Cn ({b₁} \/ {b₂}) = Cn {(b₁ '&' b₂)}

proof end;

theorem Th93: :: CQC_THE2:93

for b₁, b₂, b₃ being Element of CQC-WFF holds
( {b₁,b₂} |- b₃ iff {(b₁ '&' b₂)} |- b₃ )

proof end;

theorem Th94: :: CQC_THE2:94

for b₁ being Subset of CQC-WFF
for b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st b₁ |- b₂ holds
b₁ |- All b₃,b₂

proof end;

theorem Th95: :: CQC_THE2:95

for b₁ being Subset of CQC-WFF
for b₂, b₃ being Element of CQC-WFF
for b₄ being bound_QC-variable st not b₄ in still_not-bound_in b₂ holds
b₁ |- (All b₄,(b₂ => b₃)) => (b₂ => (All b₄,b₃))

proof end;

theorem Th96: :: CQC_THE2:96

for b₁ being Subset of CQC-WFF
for b₂, b₃ being Element of CQC-WFF st b₂ is closed & b₁ \/ {b₂} |- b₃ holds
b₁ |- b₂ => b₃

proof end;