let s be QC-formula; :: thesis: for y, x being bound_QC-variable st s . y in CQC-WFF & not x in still_not-bound_in s & s . x is valid holds
s . y is valid
let y, x be bound_QC-variable; :: thesis: ( s . y in CQC-WFF & 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 & not x in still_not-bound_in s ) and
A2: s . x is valid ; :: thesis: s . y is valid
A3: s . x in TAUT by A2, Lm13;
A4: s . y in TAUT by A1, A3, Th35;
thus s . y is valid by A4, Lm13; :: thesis: verum