let Y, X be Subset of CQC-WFF ; :: thesis: ( Y = { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) } implies Y is being_a_theory )
assume A1: Y = { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) } ; :: thesis: Y is being_a_theory
hence VERUM in Y by Lm3; :: 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 Y & p => (('not' p) => q) in Y & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y & (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All x,p) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All x,q) in Y ) & ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) )
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 Y & p => (('not' p) => q) in Y & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y & (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All x,p) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All x,q) in Y ) & ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) )
let s be QC-formula; :: thesis: for x, y being bound_QC-variable holds
( (('not' p) => p) => p in Y & p => (('not' p) => q) in Y & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y & (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All x,p) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All x,q) in Y ) & ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) )
let x, y be bound_QC-variable; :: thesis: ( (('not' p) => p) => p in Y & p => (('not' p) => q) in Y & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y & (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All x,p) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All x,q) in Y ) & ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) )
thus (('not' p) => p) => p in Y by A1, Lm4; :: thesis: ( p => (('not' p) => q) in Y & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y & (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All x,p) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All x,q) in Y ) & ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) )
thus p => (('not' p) => q) in Y by A1, Lm5; :: thesis: ( (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y & (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All x,p) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All x,q) in Y ) & ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) )
thus (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y by A1, Lm6; :: thesis: ( (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All x,p) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All x,q) in Y ) & ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) )
thus (p '&' q) => (q '&' p) in Y by A1, Lm7; :: thesis: ( ( p in Y & p => q in Y implies q in Y ) & (All x,p) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All x,q) in Y ) & ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) )
thus ( p in Y & p => q in Y implies q in Y ) by A1, Lm8; :: thesis: ( (All x,p) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All x,q) in Y ) & ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) )
thus (All x,p) => p in Y by A1, Lm9; :: thesis: ( ( p => q in Y & not x in still_not-bound_in p implies p => (All x,q) in Y ) & ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) )
thus ( p => q in Y & not x in still_not-bound_in p implies p => (All x,q) in Y ) by A1, Lm10; :: thesis: ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Y implies s . y in Y )
thus ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) by A1, Lm11; :: thesis: verum