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 that
A1: s . x in CQC-WFF and
A2: s . y in CQC-WFF and
A3: not x in still_not-bound_in s and
A4: s . x in Cn X ; :: thesis: s . y in Cn X
reconsider s1 = s . x as Element of CQC-WFF by A1;
reconsider q = s . y as Element of CQC-WFF by A2;
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 that
A5: T is being_a_theory and
A6: X c= T ; :: thesis: q in T
s1 in T by A4, A5, A6, Def2;
hence q in T by A3, A5, Def1; :: thesis: verum

end;

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