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
s . x in Cn X by A2, Def9;
then s . y in Cn X by A1, Th35;
hence X |- s . y by Def9; :: thesis: verum