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 is valid holds
s . y is valid
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 is valid implies s . y is valid )
assume ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x is valid ) ; :: thesis: s . y is valid
then ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in TAUT ) by Lm13;
then s . y in TAUT by Th35;
hence s . y is valid by Lm13; :: thesis: verum