let X be Subset of CQC-WFF ; :: thesis: for s being QC-formula
for x, y being bound_QC-variable st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Cn X holds
s . y in Cn X
let s be QC-formula; :: thesis: for x, y being bound_QC-variable st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Cn X holds
s . y in Cn X
let x, y be bound_QC-variable; :: thesis: ( 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 )
assume A1: ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Cn X ) ; :: thesis: s . y in Cn X
then reconsider s1 = s . x as Element of CQC-WFF ;
reconsider q = s . y as Element of CQC-WFF by A1;
for T being Subset of CQC-WFF st T is being_a_theory & X c= T holds
q in T

proof

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

end;

hence s . y in Cn X by Def2; :: thesis: verum