let X be Subset of CQC-WFF ; :: thesis: for s being QC-formula
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 & X |- s . x holds
X |- s . y
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 & X |- s . x holds
X |- s . y
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 & X |- s . x implies X |- s . y )
assume ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & X |- s . x ) ; :: thesis: X |- s . y
then ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Cn X ) by Def9;
then s . y in Cn X by Th35;
hence X |- s . y by Def9; :: thesis: verum