let Al be QC-alphabet ; :: thesis: for s being QC-formula of Al
for y, x being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x is valid holds
s . y is valid
let s be QC-formula of Al; :: thesis: for y, x being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x is valid holds
s . y is valid
let y, x be bound_QC-variable of Al; :: thesis: ( s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x is valid implies s . y is valid )
assume that
A1: ( s . y in CQC-WFF Al & not x in still_not-bound_in s ) and
A2: s . x is valid ; :: thesis: s . y is valid
s . x in TAUT Al by A2, Lm13;
then s . y in TAUT Al by A1, Th14;
hence s . y is valid by Lm13; :: thesis: verum