let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al) holds Cn X is being_a_theory
let X be Subset of (CQC-WFF Al); :: thesis: Cn X is being_a_theory
thus VERUM Al in Cn X by Th6; :: according to CQC_THE1:def 1 :: thesis: for p, q, r being Element of CQC-WFF Al
for s being QC-formula of Al
for x, y being bound_QC-variable of Al holds
( (('not' p) => p) => p in Cn X & p => (('not' p) => q) in Cn X & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X & (p '&' q) => (q '&' p) in Cn X & ( p in Cn X & p => q in Cn X implies q in Cn X ) & (All (x,p)) => p in Cn X & ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Cn X implies s . y in Cn X ) )
let p, q, r be Element of CQC-WFF Al; :: thesis: for s being QC-formula of Al
for x, y being bound_QC-variable of Al holds
( (('not' p) => p) => p in Cn X & p => (('not' p) => q) in Cn X & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X & (p '&' q) => (q '&' p) in Cn X & ( p in Cn X & p => q in Cn X implies q in Cn X ) & (All (x,p)) => p in Cn X & ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Cn X implies s . y in Cn X ) )
let s be QC-formula of Al; :: thesis: for x, y being bound_QC-variable of Al holds
( (('not' p) => p) => p in Cn X & p => (('not' p) => q) in Cn X & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X & (p '&' q) => (q '&' p) in Cn X & ( p in Cn X & p => q in Cn X implies q in Cn X ) & (All (x,p)) => p in Cn X & ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Cn X implies s . y in Cn X ) )
let x, y be bound_QC-variable of Al; :: thesis: ( (('not' p) => p) => p in Cn X & p => (('not' p) => q) in Cn X & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X & (p '&' q) => (q '&' p) in Cn X & ( p in Cn X & p => q in Cn X implies q in Cn X ) & (All (x,p)) => p in Cn X & ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Cn X implies s . y in Cn X ) )
thus ( (('not' p) => p) => p in Cn X & p => (('not' p) => q) in Cn X & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X & (p '&' q) => (q '&' p) in Cn X & ( p in Cn X & p => q in Cn X implies q in Cn X ) ) by Th7, Th8, Th9, Th10, Th11; :: thesis: ( (All (x,p)) => p in Cn X & ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Cn X implies s . y in Cn X ) )
thus ( (All (x,p)) => p in Cn X & ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Cn X implies s . y in Cn X ) ) by Th12, Th13, Th14; :: thesis: verum