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