let X be Subset of CQC-WFF ; :: thesis: for s being QC-formula
for y, x being bound_QC-variable st s . y in CQC-WFF & not x in still_not-bound_in s & X |- s . x holds
X |- s . y
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 & X |- s . x holds
X |- s . y
let y, x be bound_QC-variable; :: thesis: ( s . y in CQC-WFF & not x in still_not-bound_in s & X |- s . x implies X |- s . y )
assume that
A1: ( s . y in CQC-WFF & not x in still_not-bound_in s ) and
A2: X |- s . x ; :: thesis: X |- s . y
A3: s . x in Cn X by A2, Def9;
A4: s . y in Cn X by A1, A3, Th35;
thus X |- s . y by A4, Def9; :: thesis: verum