:: CQC_THE1 semantic presentation

theorem Th1: :: CQC_THE1:1
canceled;

theorem Th2: :: CQC_THE1:2
for b1 being natural number holds
( not b1 <= 1 or b1 = 0 or b1 = 1 )
proof end;

theorem Th3: :: CQC_THE1:3
for b1 being natural number holds
( not b1 <= 2 or b1 = 0 or b1 = 1 or b1 = 2 )
proof end;

theorem Th4: :: CQC_THE1:4
for b1 being natural number holds
( not b1 <= 3 or b1 = 0 or b1 = 1 or b1 = 2 or b1 = 3 )
proof end;

theorem Th5: :: CQC_THE1:5
for b1 being natural number holds
( not b1 <= 4 or b1 = 0 or b1 = 1 or b1 = 2 or b1 = 3 or b1 = 4 )
proof end;

theorem Th6: :: CQC_THE1:6
for b1 being natural number holds
( not b1 <= 5 or b1 = 0 or b1 = 1 or b1 = 2 or b1 = 3 or b1 = 4 or b1 = 5 )
proof end;

theorem Th7: :: CQC_THE1:7
for b1 being natural number holds
( not b1 <= 6 or b1 = 0 or b1 = 1 or b1 = 2 or b1 = 3 or b1 = 4 or b1 = 5 or b1 = 6 )
proof end;

theorem Th8: :: CQC_THE1:8
for b1 being natural number holds
( not b1 <= 7 or b1 = 0 or b1 = 1 or b1 = 2 or b1 = 3 or b1 = 4 or b1 = 5 or b1 = 6 or b1 = 7 )
proof end;

theorem Th9: :: CQC_THE1:9
for b1 being natural number holds
( not b1 <= 8 or b1 = 0 or b1 = 1 or b1 = 2 or b1 = 3 or b1 = 4 or b1 = 5 or b1 = 6 or b1 = 7 or b1 = 8 )
proof end;

theorem Th10: :: CQC_THE1:10
for b1 being natural number holds
( not b1 <= 9 or b1 = 0 or b1 = 1 or b1 = 2 or b1 = 3 or b1 = 4 or b1 = 5 or b1 = 6 or b1 = 7 or b1 = 8 or b1 = 9 )
proof end;

theorem Th11: :: CQC_THE1:11
for b1 being Nat holds { b2 where B is Nat : b2 <= b1 + 1 } = { b2 where B is Nat : b2 <= b1 } \/ {(b1 + 1)}
proof end;

theorem Th12: :: CQC_THE1:12
for b1 being Nat holds { b2 where B is Nat : b2 <= b1 } is finite
proof end;

deffunc H1( set ) -> set = a1 `1 ;

theorem Th13: :: CQC_THE1:13
for b1, b2, b3 being set st b1 is finite & b1 c= [:b2,b3:] holds
ex b4, b5 being set st
( b4 is finite & b4 c= b2 & b5 is finite & b5 c= b3 & b1 c= [:b4,b5:] )
proof end;

theorem Th14: :: CQC_THE1:14
for b1, b2, b3 being set st b1 is finite & b2 is finite & b1 c= [:b3,b2:] holds
ex b4 being set st
( b4 is finite & b4 c= b3 & b1 c= [:b4,b2:] )
proof end;

definition
let c1 be Subset of CQC-WFF ;
attr a1 is being_a_theory means :Def1: :: CQC_THE1:def 1
( VERUM in a1 & ( for b1, b2, b3 being Element of CQC-WFF
for b4 being QC-formula
for b5, b6 being bound_QC-variable holds
( (('not' b1) => b1) => b1 in a1 & b1 => (('not' b1) => b2) in a1 & (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) in a1 & (b1 '&' b2) => (b2 '&' b1) in a1 & ( b1 in a1 & b1 => b2 in a1 implies b2 in a1 ) & (All b5,b1) => b1 in a1 & ( b1 => b2 in a1 & not b5 in still_not-bound_in b1 implies b1 => (All b5,b2) in a1 ) & ( b4 . b5 in CQC-WFF & b4 . b6 in CQC-WFF & not b5 in still_not-bound_in b4 & b4 . b5 in a1 implies b4 . b6 in a1 ) ) ) );
end;

:: deftheorem Def1 defines being_a_theory CQC_THE1:def 1 :
for b1 being Subset of CQC-WFF holds
( b1 is being_a_theory iff ( VERUM in b1 & ( for b2, b3, b4 being Element of CQC-WFF
for b5 being QC-formula
for b6, b7 being bound_QC-variable holds
( (('not' b2) => b2) => b2 in b1 & b2 => (('not' b2) => b3) in b1 & (b2 => b3) => (('not' (b3 '&' b4)) => ('not' (b2 '&' b4))) in b1 & (b2 '&' b3) => (b3 '&' b2) in b1 & ( b2 in b1 & b2 => b3 in b1 implies b3 in b1 ) & (All b6,b2) => b2 in b1 & ( b2 => b3 in b1 & not b6 in still_not-bound_in b2 implies b2 => (All b6,b3) in b1 ) & ( b5 . b6 in CQC-WFF & b5 . b7 in CQC-WFF & not b6 in still_not-bound_in b5 & b5 . b6 in b1 implies b5 . b7 in b1 ) ) ) ) );

notation
let c1 be Subset of CQC-WFF ;
synonym c1 is_a_theory for being_a_theory c1;
end;

theorem Th15: :: CQC_THE1:15
canceled;

theorem Th16: :: CQC_THE1:16
canceled;

theorem Th17: :: CQC_THE1:17
canceled;

theorem Th18: :: CQC_THE1:18
canceled;

theorem Th19: :: CQC_THE1:19
canceled;

theorem Th20: :: CQC_THE1:20
canceled;

theorem Th21: :: CQC_THE1:21
canceled;

theorem Th22: :: CQC_THE1:22
canceled;

theorem Th23: :: CQC_THE1:23
canceled;

theorem Th24: :: CQC_THE1:24
canceled;

theorem Th25: :: CQC_THE1:25
for b1, b2 being Subset of CQC-WFF st b1 is_a_theory & b2 is_a_theory holds
b1 /\ b2 is_a_theory
proof end;

definition
let c1 be Subset of CQC-WFF ;
func Cn c1 -> Subset of CQC-WFF means :Def2: :: CQC_THE1:def 2
for b1 being Element of CQC-WFF holds
( b1 in a2 iff for b2 being Subset of CQC-WFF st b2 is_a_theory & a1 c= b2 holds
b1 in b2 );
existence
ex b1 being Subset of CQC-WFF st
for b2 being Element of CQC-WFF holds
( b2 in b1 iff for b3 being Subset of CQC-WFF st b3 is_a_theory & c1 c= b3 holds
b2 in b3 )
proof end;
uniqueness
for b1, b2 being Subset of CQC-WFF st ( for b3 being Element of CQC-WFF holds
( b3 in b1 iff for b4 being Subset of CQC-WFF st b4 is_a_theory & c1 c= b4 holds
b3 in b4 ) ) & ( for b3 being Element of CQC-WFF holds
( b3 in b2 iff for b4 being Subset of CQC-WFF st b4 is_a_theory & c1 c= b4 holds
b3 in b4 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Cn CQC_THE1:def 2 :
for b1, b2 being Subset of CQC-WFF holds
( b2 = Cn b1 iff for b3 being Element of CQC-WFF holds
( b3 in b2 iff for b4 being Subset of CQC-WFF st b4 is_a_theory & b1 c= b4 holds
b3 in b4 ) );

theorem Th26: :: CQC_THE1:26
canceled;

theorem Th27: :: CQC_THE1:27
for b1 being Subset of CQC-WFF holds VERUM in Cn b1
proof end;

theorem Th28: :: CQC_THE1:28
for b1 being Subset of CQC-WFF
for b2 being Element of CQC-WFF holds (('not' b2) => b2) => b2 in Cn b1
proof end;

theorem Th29: :: CQC_THE1:29
for b1 being Subset of CQC-WFF
for b2, b3 being Element of CQC-WFF holds b2 => (('not' b2) => b3) in Cn b1
proof end;

theorem Th30: :: CQC_THE1:30
for b1 being Subset of CQC-WFF
for b2, b3, b4 being Element of CQC-WFF holds (b2 => b3) => (('not' (b3 '&' b4)) => ('not' (b2 '&' b4))) in Cn b1
proof end;

theorem Th31: :: CQC_THE1:31
for b1 being Subset of CQC-WFF
for b2, b3 being Element of CQC-WFF holds (b2 '&' b3) => (b3 '&' b2) in Cn b1
proof end;

theorem Th32: :: CQC_THE1:32
for b1 being Subset of CQC-WFF
for b2, b3 being Element of CQC-WFF st b2 in Cn b1 & b2 => b3 in Cn b1 holds
b3 in Cn b1
proof end;

theorem Th33: :: CQC_THE1:33
for b1 being Subset of CQC-WFF
for b2 being Element of CQC-WFF
for b3 being bound_QC-variable holds (All b3,b2) => b2 in Cn b1
proof end;

theorem Th34: :: CQC_THE1:34
for b1 being Subset of CQC-WFF
for b2, b3 being Element of CQC-WFF
for b4 being bound_QC-variable st b2 => b3 in Cn b1 & not b4 in still_not-bound_in b2 holds
b2 => (All b4,b3) in Cn b1
proof end;

theorem Th35: :: CQC_THE1:35
for b1 being Subset of CQC-WFF
for b2 being QC-formula
for b3, b4 being bound_QC-variable st b2 . b3 in CQC-WFF & b2 . b4 in CQC-WFF & not b3 in still_not-bound_in b2 & b2 . b3 in Cn b1 holds
b2 . b4 in Cn b1
proof end;

theorem Th36: :: CQC_THE1:36
for b1 being Subset of CQC-WFF holds Cn b1 is_a_theory
proof end;

theorem Th37: :: CQC_THE1:37
for b1, b2 being Subset of CQC-WFF st b1 is_a_theory & b2 c= b1 holds
Cn b2 c= b1
proof end;

theorem Th38: :: CQC_THE1:38
for b1 being Subset of CQC-WFF holds b1 c= Cn b1
proof end;

theorem Th39: :: CQC_THE1:39
for b1, b2 being Subset of CQC-WFF st b1 c= b2 holds
Cn b1 c= Cn b2
proof end;

Lemma20: for b1 being Subset of CQC-WFF holds Cn (Cn b1) c= Cn b1
proof end;

theorem Th40: :: CQC_THE1:40
for b1 being Subset of CQC-WFF holds Cn (Cn b1) = Cn b1
proof end;

theorem Th41: :: CQC_THE1:41
for b1 being Subset of CQC-WFF holds
( b1 is_a_theory iff Cn b1 = b1 )
proof end;

definition
func Proof_Step_Kinds -> set equals :: CQC_THE1:def 3
{ b1 where B is Nat : b1 <= 9 } ;
coherence
{ b1 where B is Nat : b1 <= 9 } is set ;
end;

:: deftheorem Def3 defines Proof_Step_Kinds CQC_THE1:def 3 :
Proof_Step_Kinds = { b1 where B is Nat : b1 <= 9 } ;

registration
cluster Proof_Step_Kinds -> non empty ;
coherence
not Proof_Step_Kinds is empty
proof end;
end;

theorem Th42: :: CQC_THE1:42
canceled;

theorem Th43: :: CQC_THE1:43
( 0 in Proof_Step_Kinds & 1 in Proof_Step_Kinds & 2 in Proof_Step_Kinds & 3 in Proof_Step_Kinds & 4 in Proof_Step_Kinds & 5 in Proof_Step_Kinds & 6 in Proof_Step_Kinds & 7 in Proof_Step_Kinds & 8 in Proof_Step_Kinds & 9 in Proof_Step_Kinds ) ;

theorem Th44: :: CQC_THE1:44
Proof_Step_Kinds is finite by Th12;

theorem Th45: :: CQC_THE1:45
for b1 being Nat
for b2 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st 1 <= b1 & b1 <= len b2 & not (b2 . b1) `2 = 0 & not (b2 . b1) `2 = 1 & not (b2 . b1) `2 = 2 & not (b2 . b1) `2 = 3 & not (b2 . b1) `2 = 4 & not (b2 . b1) `2 = 5 & not (b2 . b1) `2 = 6 & not (b2 . b1) `2 = 7 & not (b2 . b1) `2 = 8 holds
(b2 . b1) `2 = 9
proof end;

definition
let c1 be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :];
let c2 be Nat;
let c3 be Subset of CQC-WFF ;
pred c1,c2 is_a_correct_step_wrt c3 means :Def4: :: CQC_THE1:def 4
(a1 . a2) `1 in a3 if (a1 . a2) `2 = 0
(a1 . a2) `1 = VERUM if (a1 . a2) `2 = 1
ex b1 being Element of CQC-WFF st (a1 . a2) `1 = (('not' b1) => b1) => b1 if (a1 . a2) `2 = 2
ex b1, b2 being Element of CQC-WFF st (a1 . a2) `1 = b1 => (('not' b1) => b2) if (a1 . a2) `2 = 3
ex b1, b2, b3 being Element of CQC-WFF st (a1 . a2) `1 = (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) if (a1 . a2) `2 = 4
ex b1, b2 being Element of CQC-WFF st (a1 . a2) `1 = (b1 '&' b2) => (b2 '&' b1) if (a1 . a2) `2 = 5
ex b1 being Element of CQC-WFF ex b2 being bound_QC-variable st (a1 . a2) `1 = (All b2,b1) => b1 if (a1 . a2) `2 = 6
ex b1, b2 being Natex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < a2 & 1 <= b2 & b2 < b1 & b3 = (a1 . b2) `1 & b4 = (a1 . a2) `1 & (a1 . b1) `1 = b3 => b4 ) if (a1 . a2) `2 = 7
ex b1 being Natex b2, b3 being Element of CQC-WFF ex b4 being bound_QC-variable st
( 1 <= b1 & b1 < a2 & (a1 . b1) `1 = b2 => b3 & not b4 in still_not-bound_in b2 & (a1 . a2) `1 = b2 => (All b4,b3) ) if (a1 . a2) `2 = 8
ex b1 being Natex b2, b3 being bound_QC-variableex b4 being QC-formula st
( 1 <= b1 & b1 < a2 & b4 . b2 in CQC-WFF & b4 . b3 in CQC-WFF & not b2 in still_not-bound_in b4 & b4 . b2 = (a1 . b1) `1 & b4 . b3 = (a1 . a2) `1 ) if (a1 . a2) `2 = 9
;
consistency
( ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 1 implies ( (c1 . c2) `1 in c3 iff (c1 . c2) `1 = VERUM ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 2 implies ( (c1 . c2) `1 in c3 iff ex b1 being Element of CQC-WFF st (c1 . c2) `1 = (('not' b1) => b1) => b1 ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 3 implies ( (c1 . c2) `1 in c3 iff ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = b1 => (('not' b1) => b2) ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 4 implies ( (c1 . c2) `1 in c3 iff ex b1, b2, b3 being Element of CQC-WFF st (c1 . c2) `1 = (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 5 implies ( (c1 . c2) `1 in c3 iff ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = (b1 '&' b2) => (b2 '&' b1) ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 6 implies ( (c1 . c2) `1 in c3 iff ex b1 being Element of CQC-WFF ex b2 being bound_QC-variable st (c1 . c2) `1 = (All b2,b1) => b1 ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 7 implies ( (c1 . c2) `1 in c3 iff ex b1, b2 being Natex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & b3 = (c1 . b2) `1 & b4 = (c1 . c2) `1 & (c1 . b1) `1 = b3 => b4 ) ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 8 implies ( (c1 . c2) `1 in c3 iff ex b1 being Natex b2, b3 being Element of CQC-WFF ex b4 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & (c1 . b1) `1 = b2 => b3 & not b4 in still_not-bound_in b2 & (c1 . c2) `1 = b2 => (All b4,b3) ) ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 9 implies ( (c1 . c2) `1 in c3 iff ex b1 being Natex b2, b3 being bound_QC-variableex b4 being QC-formula st
( 1 <= b1 & b1 < c2 & b4 . b2 in CQC-WFF & b4 . b3 in CQC-WFF & not b2 in still_not-bound_in b4 & b4 . b2 = (c1 . b1) `1 & b4 . b3 = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 2 implies ( (c1 . c2) `1 = VERUM iff ex b1 being Element of CQC-WFF st (c1 . c2) `1 = (('not' b1) => b1) => b1 ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 3 implies ( (c1 . c2) `1 = VERUM iff ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = b1 => (('not' b1) => b2) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 4 implies ( (c1 . c2) `1 = VERUM iff ex b1, b2, b3 being Element of CQC-WFF st (c1 . c2) `1 = (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 5 implies ( (c1 . c2) `1 = VERUM iff ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = (b1 '&' b2) => (b2 '&' b1) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 6 implies ( (c1 . c2) `1 = VERUM iff ex b1 being Element of CQC-WFF ex b2 being bound_QC-variable st (c1 . c2) `1 = (All b2,b1) => b1 ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 7 implies ( (c1 . c2) `1 = VERUM iff ex b1, b2 being Natex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & b3 = (c1 . b2) `1 & b4 = (c1 . c2) `1 & (c1 . b1) `1 = b3 => b4 ) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 8 implies ( (c1 . c2) `1 = VERUM iff ex b1 being Natex b2, b3 being Element of CQC-WFF ex b4 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & (c1 . b1) `1 = b2 => b3 & not b4 in still_not-bound_in b2 & (c1 . c2) `1 = b2 => (All b4,b3) ) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 9 implies ( (c1 . c2) `1 = VERUM iff ex b1 being Natex b2, b3 being bound_QC-variableex b4 being QC-formula st
( 1 <= b1 & b1 < c2 & b4 . b2 in CQC-WFF & b4 . b3 in CQC-WFF & not b2 in still_not-bound_in b4 & b4 . b2 = (c1 . b1) `1 & b4 . b3 = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 3 implies ( ex b1 being Element of CQC-WFF st (c1 . c2) `1 = (('not' b1) => b1) => b1 iff ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = b1 => (('not' b1) => b2) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 4 implies ( ex b1 being Element of CQC-WFF st (c1 . c2) `1 = (('not' b1) => b1) => b1 iff ex b1, b2, b3 being Element of CQC-WFF st (c1 . c2) `1 = (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 5 implies ( ex b1 being Element of CQC-WFF st (c1 . c2) `1 = (('not' b1) => b1) => b1 iff ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = (b1 '&' b2) => (b2 '&' b1) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 6 implies ( ex b1 being Element of CQC-WFF st (c1 . c2) `1 = (('not' b1) => b1) => b1 iff ex b1 being Element of CQC-WFF ex b2 being bound_QC-variable st (c1 . c2) `1 = (All b2,b1) => b1 ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 7 implies ( ex b1 being Element of CQC-WFF st (c1 . c2) `1 = (('not' b1) => b1) => b1 iff ex b1, b2 being Natex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & b3 = (c1 . b2) `1 & b4 = (c1 . c2) `1 & (c1 . b1) `1 = b3 => b4 ) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 8 implies ( ex b1 being Element of CQC-WFF st (c1 . c2) `1 = (('not' b1) => b1) => b1 iff ex b1 being Natex b2, b3 being Element of CQC-WFF ex b4 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & (c1 . b1) `1 = b2 => b3 & not b4 in still_not-bound_in b2 & (c1 . c2) `1 = b2 => (All b4,b3) ) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 9 implies ( ex b1 being Element of CQC-WFF st (c1 . c2) `1 = (('not' b1) => b1) => b1 iff ex b1 being Natex b2, b3 being bound_QC-variableex b4 being QC-formula st
( 1 <= b1 & b1 < c2 & b4 . b2 in CQC-WFF & b4 . b3 in CQC-WFF & not b2 in still_not-bound_in b4 & b4 . b2 = (c1 . b1) `1 & b4 . b3 = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 3 & (c1 . c2) `2 = 4 implies ( ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = b1 => (('not' b1) => b2) iff ex b1, b2, b3 being Element of CQC-WFF st (c1 . c2) `1 = (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) ) ) & ( (c1 . c2) `2 = 3 & (c1 . c2) `2 = 5 implies ( ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = b1 => (('not' b1) => b2) iff ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = (b1 '&' b2) => (b2 '&' b1) ) ) & ( (c1 . c2) `2 = 3 & (c1 . c2) `2 = 6 implies ( ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = b1 => (('not' b1) => b2) iff ex b1 being Element of CQC-WFF ex b2 being bound_QC-variable st (c1 . c2) `1 = (All b2,b1) => b1 ) ) & ( (c1 . c2) `2 = 3 & (c1 . c2) `2 = 7 implies ( ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = b1 => (('not' b1) => b2) iff ex b1, b2 being Natex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & b3 = (c1 . b2) `1 & b4 = (c1 . c2) `1 & (c1 . b1) `1 = b3 => b4 ) ) ) & ( (c1 . c2) `2 = 3 & (c1 . c2) `2 = 8 implies ( ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = b1 => (('not' b1) => b2) iff ex b1 being Natex b2, b3 being Element of CQC-WFF ex b4 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & (c1 . b1) `1 = b2 => b3 & not b4 in still_not-bound_in b2 & (c1 . c2) `1 = b2 => (All b4,b3) ) ) ) & ( (c1 . c2) `2 = 3 & (c1 . c2) `2 = 9 implies ( ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = b1 => (('not' b1) => b2) iff ex b1 being Natex b2, b3 being bound_QC-variableex b4 being QC-formula st
( 1 <= b1 & b1 < c2 & b4 . b2 in CQC-WFF & b4 . b3 in CQC-WFF & not b2 in still_not-bound_in b4 & b4 . b2 = (c1 . b1) `1 & b4 . b3 = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 4 & (c1 . c2) `2 = 5 implies ( ex b1, b2, b3 being Element of CQC-WFF st (c1 . c2) `1 = (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) iff ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = (b1 '&' b2) => (b2 '&' b1) ) ) & ( (c1 . c2) `2 = 4 & (c1 . c2) `2 = 6 implies ( ex b1, b2, b3 being Element of CQC-WFF st (c1 . c2) `1 = (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) iff ex b1 being Element of CQC-WFF ex b2 being bound_QC-variable st (c1 . c2) `1 = (All b2,b1) => b1 ) ) & ( (c1 . c2) `2 = 4 & (c1 . c2) `2 = 7 implies ( ex b1, b2, b3 being Element of CQC-WFF st (c1 . c2) `1 = (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) iff ex b1, b2 being Natex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & b3 = (c1 . b2) `1 & b4 = (c1 . c2) `1 & (c1 . b1) `1 = b3 => b4 ) ) ) & ( (c1 . c2) `2 = 4 & (c1 . c2) `2 = 8 implies ( ex b1, b2, b3 being Element of CQC-WFF st (c1 . c2) `1 = (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) iff ex b1 being Natex b2, b3 being Element of CQC-WFF ex b4 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & (c1 . b1) `1 = b2 => b3 & not b4 in still_not-bound_in b2 & (c1 . c2) `1 = b2 => (All b4,b3) ) ) ) & ( (c1 . c2) `2 = 4 & (c1 . c2) `2 = 9 implies ( ex b1, b2, b3 being Element of CQC-WFF st (c1 . c2) `1 = (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) iff ex b1 being Natex b2, b3 being bound_QC-variableex b4 being QC-formula st
( 1 <= b1 & b1 < c2 & b4 . b2 in CQC-WFF & b4 . b3 in CQC-WFF & not b2 in still_not-bound_in b4 & b4 . b2 = (c1 . b1) `1 & b4 . b3 = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 5 & (c1 . c2) `2 = 6 implies ( ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = (b1 '&' b2) => (b2 '&' b1) iff ex b1 being Element of CQC-WFF ex b2 being bound_QC-variable st (c1 . c2) `1 = (All b2,b1) => b1 ) ) & ( (c1 . c2) `2 = 5 & (c1 . c2) `2 = 7 implies ( ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = (b1 '&' b2) => (b2 '&' b1) iff ex b1, b2 being Natex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & b3 = (c1 . b2) `1 & b4 = (c1 . c2) `1 & (c1 . b1) `1 = b3 => b4 ) ) ) & ( (c1 . c2) `2 = 5 & (c1 . c2) `2 = 8 implies ( ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = (b1 '&' b2) => (b2 '&' b1) iff ex b1 being Natex b2, b3 being Element of CQC-WFF ex b4 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & (c1 . b1) `1 = b2 => b3 & not b4 in still_not-bound_in b2 & (c1 . c2) `1 = b2 => (All b4,b3) ) ) ) & ( (c1 . c2) `2 = 5 & (c1 . c2) `2 = 9 implies ( ex b1, b2 being Element of CQC-WFF st (c1 . c2) `1 = (b1 '&' b2) => (b2 '&' b1) iff ex b1 being Natex b2, b3 being bound_QC-variableex b4 being QC-formula st
( 1 <= b1 & b1 < c2 & b4 . b2 in CQC-WFF & b4 . b3 in CQC-WFF & not b2 in still_not-bound_in b4 & b4 . b2 = (c1 . b1) `1 & b4 . b3 = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 6 & (c1 . c2) `2 = 7 implies ( ex b1 being Element of CQC-WFF ex b2 being bound_QC-variable st (c1 . c2) `1 = (All b2,b1) => b1 iff ex b1, b2 being Natex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & b3 = (c1 . b2) `1 & b4 = (c1 . c2) `1 & (c1 . b1) `1 = b3 => b4 ) ) ) & ( (c1 . c2) `2 = 6 & (c1 . c2) `2 = 8 implies ( ex b1 being Element of CQC-WFF ex b2 being bound_QC-variable st (c1 . c2) `1 = (All b2,b1) => b1 iff ex b1 being Natex b2, b3 being Element of CQC-WFF ex b4 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & (c1 . b1) `1 = b2 => b3 & not b4 in still_not-bound_in b2 & (c1 . c2) `1 = b2 => (All b4,b3) ) ) ) & ( (c1 . c2) `2 = 6 & (c1 . c2) `2 = 9 implies ( ex b1 being Element of CQC-WFF ex b2 being bound_QC-variable st (c1 . c2) `1 = (All b2,b1) => b1 iff ex b1 being Natex b2, b3 being bound_QC-variableex b4 being QC-formula st
( 1 <= b1 & b1 < c2 & b4 . b2 in CQC-WFF & b4 . b3 in CQC-WFF & not b2 in still_not-bound_in b4 & b4 . b2 = (c1 . b1) `1 & b4 . b3 = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 7 & (c1 . c2) `2 = 8 implies ( ex b1, b2 being Natex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & b3 = (c1 . b2) `1 & b4 = (c1 . c2) `1 & (c1 . b1) `1 = b3 => b4 ) iff ex b1 being Natex b2, b3 being Element of CQC-WFF ex b4 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & (c1 . b1) `1 = b2 => b3 & not b4 in still_not-bound_in b2 & (c1 . c2) `1 = b2 => (All b4,b3) ) ) ) & ( (c1 . c2) `2 = 7 & (c1 . c2) `2 = 9 implies ( ex b1, b2 being Natex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & b3 = (c1 . b2) `1 & b4 = (c1 . c2) `1 & (c1 . b1) `1 = b3 => b4 ) iff ex b1 being Natex b2, b3 being bound_QC-variableex b4 being QC-formula st
( 1 <= b1 & b1 < c2 & b4 . b2 in CQC-WFF & b4 . b3 in CQC-WFF & not b2 in still_not-bound_in b4 & b4 . b2 = (c1 . b1) `1 & b4 . b3 = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 8 & (c1 . c2) `2 = 9 implies ( ex b1 being Natex b2, b3 being Element of CQC-WFF ex b4 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & (c1 . b1) `1 = b2 => b3 & not b4 in still_not-bound_in b2 & (c1 . c2) `1 = b2 => (All b4,b3) ) iff ex b1 being Natex b2, b3 being bound_QC-variableex b4 being QC-formula st
( 1 <= b1 & b1 < c2 & b4 . b2 in CQC-WFF & b4 . b3 in CQC-WFF & not b2 in still_not-bound_in b4 & b4 . b2 = (c1 . b1) `1 & b4 . b3 = (c1 . c2) `1 ) ) ) ) ;
end;

:: deftheorem Def4 defines is_a_correct_step_wrt CQC_THE1:def 4 :
for b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :]
for b2 being Nat
for b3 being Subset of CQC-WFF holds
( ( (b1 . b2) `2 = 0 implies ( b1,b2 is_a_correct_step_wrt b3 iff (b1 . b2) `1 in b3 ) ) & ( (b1 . b2) `2 = 1 implies ( b1,b2 is_a_correct_step_wrt b3 iff (b1 . b2) `1 = VERUM ) ) & ( (b1 . b2) `2 = 2 implies ( b1,b2 is_a_correct_step_wrt b3 iff ex b4 being Element of CQC-WFF st (b1 . b2) `1 = (('not' b4) => b4) => b4 ) ) & ( (b1 . b2) `2 = 3 implies ( b1,b2 is_a_correct_step_wrt b3 iff ex b4, b5 being Element of CQC-WFF st (b1 . b2) `1 = b4 => (('not' b4) => b5) ) ) & ( (b1 . b2) `2 = 4 implies ( b1,b2 is_a_correct_step_wrt b3 iff ex b4, b5, b6 being Element of CQC-WFF st (b1 . b2) `1 = (b4 => b5) => (('not' (b5 '&' b6)) => ('not' (b4 '&' b6))) ) ) & ( (b1 . b2) `2 = 5 implies ( b1,b2 is_a_correct_step_wrt b3 iff ex b4, b5 being Element of CQC-WFF st (b1 . b2) `1 = (b4 '&' b5) => (b5 '&' b4) ) ) & ( (b1 . b2) `2 = 6 implies ( b1,b2 is_a_correct_step_wrt b3 iff ex b4 being Element of CQC-WFF ex b5 being bound_QC-variable st (b1 . b2) `1 = (All b5,b4) => b4 ) ) & ( (b1 . b2) `2 = 7 implies ( b1,b2 is_a_correct_step_wrt b3 iff ex b4, b5 being Natex b6, b7 being Element of CQC-WFF st
( 1 <= b4 & b4 < b2 & 1 <= b5 & b5 < b4 & b6 = (b1 . b5) `1 & b7 = (b1 . b2) `1 & (b1 . b4) `1 = b6 => b7 ) ) ) & ( (b1 . b2) `2 = 8 implies ( b1,b2 is_a_correct_step_wrt b3 iff ex b4 being Natex b5, b6 being Element of CQC-WFF ex b7 being bound_QC-variable st
( 1 <= b4 & b4 < b2 & (b1 . b4) `1 = b5 => b6 & not b7 in still_not-bound_in b5 & (b1 . b2) `1 = b5 => (All b7,b6) ) ) ) & ( (b1 . b2) `2 = 9 implies ( b1,b2 is_a_correct_step_wrt b3 iff ex b4 being Natex b5, b6 being bound_QC-variableex b7 being QC-formula st
( 1 <= b4 & b4 < b2 & b7 . b5 in CQC-WFF & b7 . b6 in CQC-WFF & not b5 in still_not-bound_in b7 & b7 . b5 = (b1 . b4) `1 & b7 . b6 = (b1 . b2) `1 ) ) ) );

definition
let c1 be Subset of CQC-WFF ;
let c2 be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :];
pred c2 is_a_proof_wrt c1 means :Def5: :: CQC_THE1:def 5
( a2 <> {} & ( for b1 being Nat st 1 <= b1 & b1 <= len a2 holds
a2,b1 is_a_correct_step_wrt a1 ) );
end;

:: deftheorem Def5 defines is_a_proof_wrt CQC_THE1:def 5 :
for b1 being Subset of CQC-WFF
for b2 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] holds
( b2 is_a_proof_wrt b1 iff ( b2 <> {} & ( for b3 being Nat st 1 <= b3 & b3 <= len b2 holds
b2,b3 is_a_correct_step_wrt b1 ) ) );

theorem Th46: :: CQC_THE1:46
canceled;

theorem Th47: :: CQC_THE1:47
canceled;

theorem Th48: :: CQC_THE1:48
canceled;

theorem Th49: :: CQC_THE1:49
canceled;

theorem Th50: :: CQC_THE1:50
canceled;

theorem Th51: :: CQC_THE1:51
canceled;

theorem Th52: :: CQC_THE1:52
canceled;

theorem Th53: :: CQC_THE1:53
canceled;

theorem Th54: :: CQC_THE1:54
canceled;

theorem Th55: :: CQC_THE1:55
canceled;

theorem Th56: :: CQC_THE1:56
canceled;

theorem Th57: :: CQC_THE1:57
for b1 being Subset of CQC-WFF
for b2 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st b2 is_a_proof_wrt b1 holds
rng b2 <> {}
proof end;

theorem Th58: :: CQC_THE1:58
for b1 being Subset of CQC-WFF
for b2 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st b2 is_a_proof_wrt b1 holds
1 <= len b2
proof end;

theorem Th59: :: CQC_THE1:59
for b1 being Subset of CQC-WFF
for b2 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] holds
( not b2 is_a_proof_wrt b1 or (b2 . 1) `2 = 0 or (b2 . 1) `2 = 1 or (b2 . 1) `2 = 2 or (b2 . 1) `2 = 3 or (b2 . 1) `2 = 4 or (b2 . 1) `2 = 5 or (b2 . 1) `2 = 6 )
proof end;

theorem Th60: :: CQC_THE1:60
for b1 being Nat
for b2 being Subset of CQC-WFF
for b3, b4 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st 1 <= b1 & b1 <= len b3 holds
( b3,b1 is_a_correct_step_wrt b2 iff b3 ^ b4,b1 is_a_correct_step_wrt b2 )
proof end;

theorem Th61: :: CQC_THE1:61
for b1 being Nat
for b2 being Subset of CQC-WFF
for b3, b4 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st 1 <= b1 & b1 <= len b3 & b3,b1 is_a_correct_step_wrt b2 holds
b4 ^ b3,b1 + (len b4) is_a_correct_step_wrt b2
proof end;

theorem Th62: :: CQC_THE1:62
for b1 being Subset of CQC-WFF
for b2, b3 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st b2 is_a_proof_wrt b1 & b3 is_a_proof_wrt b1 holds
b2 ^ b3 is_a_proof_wrt b1
proof end;

theorem Th63: :: CQC_THE1:63
for b1, b2 being Subset of CQC-WFF
for b3 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st b3 is_a_proof_wrt b1 & b1 c= b2 holds
b3 is_a_proof_wrt b2
proof end;

theorem Th64: :: CQC_THE1:64
for b1 being Nat
for b2 being Subset of CQC-WFF
for b3 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st b3 is_a_proof_wrt b2 & 1 <= b1 & b1 <= len b3 holds
(b3 . b1) `1 in Cn b2
proof end;

definition
let c1 be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :];
assume E31: c1 <> {} ;
func Effect c1 -> Element of CQC-WFF equals :Def6: :: CQC_THE1:def 6
(a1 . (len a1)) `1 ;
coherence
(c1 . (len c1)) `1 is Element of CQC-WFF
proof end;
end;

:: deftheorem Def6 defines Effect CQC_THE1:def 6 :
for b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st b1 <> {} holds
Effect b1 = (b1 . (len b1)) `1 ;

theorem Th65: :: CQC_THE1:65
canceled;

theorem Th66: :: CQC_THE1:66
for b1 being Subset of CQC-WFF
for b2 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st b2 is_a_proof_wrt b1 holds
Effect b2 in Cn b1
proof end;

Lemma33: for b1 being Subset of CQC-WFF holds { b2 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b3 is_a_proof_wrt b1 & Effect b3 = b2 ) } c= CQC-WFF
proof end;

theorem Th67: :: CQC_THE1:67
for b1 being Subset of CQC-WFF holds b1 c= { b2 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b3 is_a_proof_wrt b1 & Effect b3 = b2 ) }
proof end;

Lemma35: for b1 being Subset of CQC-WFF holds VERUM in { b2 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b3 is_a_proof_wrt b1 & Effect b3 = b2 ) }
proof end;

Lemma36: for b1 being Element of CQC-WFF
for b2 being Subset of CQC-WFF holds (('not' b1) => b1) => b1 in { b3 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b4 is_a_proof_wrt b2 & Effect b4 = b3 ) }
proof end;

Lemma37: for b1, b2 being Element of CQC-WFF
for b3 being Subset of CQC-WFF holds b1 => (('not' b1) => b2) in { b4 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b5 is_a_proof_wrt b3 & Effect b5 = b4 ) }
proof end;

Lemma38: for b1, b2, b3 being Element of CQC-WFF
for b4 being Subset of CQC-WFF holds (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) in { b5 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b6 is_a_proof_wrt b4 & Effect b6 = b5 ) }
proof end;

Lemma39: for b1, b2 being Element of CQC-WFF
for b3 being Subset of CQC-WFF holds (b1 '&' b2) => (b2 '&' b1) in { b4 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b5 is_a_proof_wrt b3 & Effect b5 = b4 ) }
proof end;

Lemma40: for b1, b2 being Element of CQC-WFF
for b3 being Subset of CQC-WFF st b1 in { b4 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b5 is_a_proof_wrt b3 & Effect b5 = b4 ) } & b1 => b2 in { b4 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b5 is_a_proof_wrt b3 & Effect b5 = b4 ) } holds
b2 in { b4 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b5 is_a_proof_wrt b3 & Effect b5 = b4 ) }
proof end;

Lemma41: for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being Subset of CQC-WFF holds (All b2,b1) => b1 in { b4 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b5 is_a_proof_wrt b3 & Effect b5 = b4 ) }
proof end;

Lemma42: for b1, b2 being Element of CQC-WFF
for b3 being bound_QC-variable
for b4 being Subset of CQC-WFF st b1 => b2 in { b5 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b6 is_a_proof_wrt b4 & Effect b6 = b5 ) } & not b3 in still_not-bound_in b1 holds
b1 => (All b3,b2) in { b5 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b6 is_a_proof_wrt b4 & Effect b6 = b5 ) }
proof end;

Lemma43: for b1 being QC-formula
for b2, b3 being bound_QC-variable
for b4 being Subset of CQC-WFF st b1 . b2 in CQC-WFF & b1 . b3 in CQC-WFF & not b2 in still_not-bound_in b1 & b1 . b2 in { b5 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b6 is_a_proof_wrt b4 & Effect b6 = b5 ) } holds
b1 . b3 in { b5 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b6 is_a_proof_wrt b4 & Effect b6 = b5 ) }
proof end;

theorem Th68: :: CQC_THE1:68
for b1, b2 being Subset of CQC-WFF st b1 = { b3 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b4 is_a_proof_wrt b2 & Effect b4 = b3 ) } holds
b1 is_a_theory
proof end;

Lemma45: for b1 being Subset of CQC-WFF holds { b2 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b3 is_a_proof_wrt b1 & Effect b3 = b2 ) } c= Cn b1
proof end;

theorem Th69: :: CQC_THE1:69
for b1 being Subset of CQC-WFF holds { b2 where B is Element of CQC-WFF : ex b1 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b3 is_a_proof_wrt b1 & Effect b3 = b2 ) } = Cn b1
proof end;

theorem Th70: :: CQC_THE1:70
for b1 being Subset of CQC-WFF
for b2 being Element of CQC-WFF holds
( b2 in Cn b1 iff ex b3 being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( b3 is_a_proof_wrt b1 & Effect b3 = b2 ) )
proof end;

theorem Th71: :: CQC_THE1:71
for b1 being Subset of CQC-WFF
for b2 being Element of CQC-WFF st b2 in Cn b1 holds
ex b3 being Subset of CQC-WFF st
( b3 c= b1 & b3 is finite & b2 in Cn b3 )
proof end;

definition
canceled;
func TAUT -> Subset of CQC-WFF equals :: CQC_THE1:def 8
 Cn ({} CQC-WFF );
correctness
coherence
Cn ({} CQC-WFF ) is Subset of CQC-WFF ;
;
end;

:: deftheorem Def7 CQC_THE1:def 7 :
canceled;

:: deftheorem Def8 defines TAUT CQC_THE1:def 8 :
TAUT = Cn ({} CQC-WFF );

theorem Th72: :: CQC_THE1:72
canceled;

theorem Th73: :: CQC_THE1:73
canceled;

theorem Th74: :: CQC_THE1:74
for b1 being Subset of CQC-WFF st b1 is_a_theory holds
TAUT c= b1
proof end;

theorem Th75: :: CQC_THE1:75
for b1 being Subset of CQC-WFF holds TAUT c= Cn b1
proof end;

theorem Th76: :: CQC_THE1:76
TAUT is_a_theory by Th36;

theorem Th77: :: CQC_THE1:77
VERUM in TAUT by Def1, Th76;

theorem Th78: :: CQC_THE1:78
for b1 being Element of CQC-WFF holds (('not' b1) => b1) => b1 in TAUT by Def1, Th76;

theorem Th79: :: CQC_THE1:79
for b1, b2 being Element of CQC-WFF holds b1 => (('not' b1) => b2) in TAUT by Def1, Th76;

theorem Th80: :: CQC_THE1:80
for b1, b2, b3 being Element of CQC-WFF holds (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) in TAUT by Def1, Th76;

theorem Th81: :: CQC_THE1:81
for b1, b2 being Element of CQC-WFF holds (b1 '&' b2) => (b2 '&' b1) in TAUT by Def1, Th76;

theorem Th82: :: CQC_THE1:82
for b1, b2 being Element of CQC-WFF st b1 in TAUT & b1 => b2 in TAUT holds
b2 in TAUT by Def1, Th76;

theorem Th83: :: CQC_THE1:83
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable holds (All b2,b1) => b1 in TAUT by Th33;

theorem Th84: :: CQC_THE1:84
for b1, b2 being Element of CQC-WFF
for b3 being bound_QC-variable st b1 => b2 in TAUT & not b3 in still_not-bound_in b1 holds
b1 => (All b3,b2) in TAUT by Th34;

theorem Th85: :: CQC_THE1:85
for b1 being QC-formula
for b2, b3 being bound_QC-variable st b1 . b2 in CQC-WFF & b1 . b3 in CQC-WFF & not b2 in still_not-bound_in b1 & b1 . b2 in TAUT holds
b1 . b3 in TAUT by Th35;

definition
let c1 be Subset of CQC-WFF ;
let c2 be QC-formula;
pred c1 |- c2 means :Def9: :: CQC_THE1:def 9
a2 in Cn a1;
end;

:: deftheorem Def9 defines |- CQC_THE1:def 9 :
for b1 being Subset of CQC-WFF
for b2 being QC-formula holds
( b1 |- b2 iff b2 in Cn b1 );

theorem Th86: :: CQC_THE1:86
canceled;

theorem Th87: :: CQC_THE1:87
for b1 being Subset of CQC-WFF holds b1 |- VERUM
proof end;

theorem Th88: :: CQC_THE1:88
for b1 being Subset of CQC-WFF
for b2 being Element of CQC-WFF holds b1 |- (('not' b2) => b2) => b2
proof end;

theorem Th89: :: CQC_THE1:89
for b1 being Subset of CQC-WFF
for b2, b3 being Element of CQC-WFF holds b1 |- b2 => (('not' b2) => b3)
proof end;

theorem Th90: :: CQC_THE1:90
for b1 being Subset of CQC-WFF
for b2, b3, b4 being Element of CQC-WFF holds b1 |- (b2 => b3) => (('not' (b3 '&' b4)) => ('not' (b2 '&' b4)))
proof end;

theorem Th91: :: CQC_THE1:91
for b1 being Subset of CQC-WFF
for b2, b3 being Element of CQC-WFF holds b1 |- (b2 '&' b3) => (b3 '&' b2)
proof end;

theorem Th92: :: CQC_THE1:92
for b1 being Subset of CQC-WFF
for b2, b3 being Element of CQC-WFF st b1 |- b2 & b1 |- b2 => b3 holds
b1 |- b3
proof end;

theorem Th93: :: CQC_THE1:93
for b1 being Subset of CQC-WFF
for b2 being Element of CQC-WFF
for b3 being bound_QC-variable holds b1 |- (All b3,b2) => b2
proof end;

theorem Th94: :: CQC_THE1:94
for b1 being Subset of CQC-WFF
for b2, b3 being Element of CQC-WFF
for b4 being bound_QC-variable st b1 |- b2 => b3 & not b4 in still_not-bound_in b2 holds
b1 |- b2 => (All b4,b3)
proof end;

theorem Th95: :: CQC_THE1:95
for b1 being Subset of CQC-WFF
for b2 being QC-formula
for b3, b4 being bound_QC-variable st b2 . b3 in CQC-WFF & b2 . b4 in CQC-WFF & not b3 in still_not-bound_in b2 & b1 |- b2 . b3 holds
b1 |- b2 . b4
proof end;

definition
let c1 be QC-formula;
attr a1 is valid means :Def10: :: CQC_THE1:def 10
 {} CQC-WFF |- a1;
end;

:: deftheorem Def10 defines valid CQC_THE1:def 10 :
for b1 being QC-formula holds
( b1 is valid iff {} CQC-WFF |- b1 );

notation
let c1 be QC-formula;
synonym |- c1 for valid c1;
end;

Lemma54: for b1 being QC-formula holds
( |-|- b1 valid b1 iff b1 in TAUT )
proof end;

definition
let c1 be QC-formula;
redefine attr a1 is valid means :: CQC_THE1:def 11
a1 in TAUT ;
compatibility
( c1 is valid iff c1 in TAUT ) by Lemma54;
end;

:: deftheorem Def11 defines valid CQC_THE1:def 11 :
for b1 being QC-formula holds
( b1 is valid iff b1 in TAUT );

theorem Th96: :: CQC_THE1:96
canceled;

theorem Th97: :: CQC_THE1:97
canceled;

theorem Th98: :: CQC_THE1:98
for b1 being Subset of CQC-WFF
for b2 being Element of CQC-WFF st |-|- b2 valid b2 holds
b1 |- b2
proof end;

theorem Th99: :: CQC_THE1:99
|-|- VERUM valid VERUM by Lemma54, Th77;

theorem Th100: :: CQC_THE1:100
for b1 being Element of CQC-WFF holds |-|- (('not' b1) => b1) => b1 valid (('not' b1) => b1) => b1
proof end;

theorem Th101: :: CQC_THE1:101
for b1, b2 being Element of CQC-WFF holds |-|- b1 => (('not' b1) => b2) valid b1 => (('not' b1) => b2)
proof end;

theorem Th102: :: CQC_THE1:102
for b1, b2, b3 being Element of CQC-WFF holds |-|- (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3))) valid (b1 => b2) => (('not' (b2 '&' b3)) => ('not' (b1 '&' b3)))
proof end;

theorem Th103: :: CQC_THE1:103
for b1, b2 being Element of CQC-WFF holds |-|- (b1 '&' b2) => (b2 '&' b1) valid (b1 '&' b2) => (b2 '&' b1)
proof end;

theorem Th104: :: CQC_THE1:104
for b1, b2 being Element of CQC-WFF st |-|- b1 valid b1 & |-|- b1 => b2 valid b1 => b2 holds
|-|- b2 valid b2
proof end;

theorem Th105: :: CQC_THE1:105
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable holds |-|- (All b2,b1) => b1 valid (All b2,b1) => b1
proof end;

theorem Th106: :: CQC_THE1:106
for b1, b2 being Element of CQC-WFF
for b3 being bound_QC-variable st |-|- b1 => b2 valid b1 => b2 & not b3 in still_not-bound_in b1 holds
|-|- b1 => (All b3,b2) valid b1 => (All b3,b2)
proof end;

theorem Th107: :: CQC_THE1:107
for b1 being QC-formula
for b2, b3 being bound_QC-variable st b1 . b2 in CQC-WFF & b1 . b3 in CQC-WFF & not b2 in still_not-bound_in b1 & |-|- b1 . b2 valid b1 . b2 holds
|-|- b1 . b3 valid b1 . b3
proof end;