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

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

hence
s . y in Cn X
by Def2; :: thesis: verum
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;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