let X be Subset of CQC-WFF; :: thesis: Cn X is being_a_theory
thus VERUM in Cn X by Th27; :: according to CQC_THE1:def 1 :: thesis: for p, q, r being Element of CQC-WFF
for s being QC-formula
for x, y being bound_QC-variable 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 & s . y in CQC-WFF & 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 ; :: thesis: for s being QC-formula
for x, y being bound_QC-variable 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 & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Cn X implies s . y in Cn X ) )
let s be QC-formula; :: thesis: for x, y being bound_QC-variable 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 & s . y in CQC-WFF & 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; :: 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 & s . y in CQC-WFF & 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 Th28, Th29, Th30, Th31, Th32; :: 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 & s . y in CQC-WFF & 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 & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Cn X implies s . y in Cn X ) ) by Th33, Th34, Th35; :: thesis: verum