:: deftheorem defines being_a_theory CQC_THE1:def 1 :
for Al being QC-alphabet
for T being Subset of (CQC-WFF Al) holds
( T is being_a_theory iff ( VERUM Al in T & ( 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 T & p => (('not' p) => q) in T & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T & (p '&' q) => (q '&' p) in T & ( p in T & p => q in T implies q in T ) & (All (x,p)) => p in T & ( p => q in T & not x in still_not-bound_in p implies p => (All (x,q)) in T ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T implies s . y in T ) ) ) ) );