let X be Subset of CQC-WFF ; :: thesis: for p, q being Element of CQC-WFF
for x being bound_QC-variable st p => q in Cn X & not x in still_not-bound_in p holds
p => (All x,q) in Cn X
let p, q be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable st p => q in Cn X & not x in still_not-bound_in p holds
p => (All x,q) in Cn X
let x be bound_QC-variable; :: thesis: ( p => q in Cn X & not x in still_not-bound_in p implies p => (All x,q) in Cn X )
assume A1: ( p => q in Cn X & not x in still_not-bound_in p ) ; :: thesis: p => (All x,q) in Cn X
for T being Subset of CQC-WFF st T is being_a_theory & X c= T holds
p => (All x,q) in T

proof

let T be Subset of CQC-WFF ; :: thesis: ( T is being_a_theory & X c= T implies p => (All x,q) in T )
assume A2: ( T is being_a_theory & X c= T ) ; :: thesis: p => (All x,q) in T
then p => q in T by A1, Def2;
hence p => (All x,q) in T by A1, A2, Def1; :: thesis: verum

end;

hence p => (All x,q) in Cn X by Def2; :: thesis: verum