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;
A5: 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
A6: T is being_a_theory and
A7: X c= T ; :: thesis: q in T
A8: s1 in T by A4, A6, A7, Def2;
thus q in T by A3, A6, A8, Def1; :: thesis: verum

end;

thus s . y in Cn X by A5, Def2; :: thesis: verum