let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for s being QC-formula of Al
for y, x being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & X |- s . x holds
X |- s . y
let X be Subset of (CQC-WFF Al); :: thesis: for s being QC-formula of Al
for y, x being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & X |- s . x holds
X |- s . y
let s be QC-formula of Al; :: thesis: for y, x being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & X |- s . x holds
X |- s . y
let y, x be bound_QC-variable of Al; :: thesis: ( s . y in CQC-WFF Al & not x in still_not-bound_in s & X |- s . x implies X |- s . y )
assume that
A1: ( s . y in CQC-WFF Al & not x in still_not-bound_in s ) and
A2: X |- s . x ; :: thesis: X |- s . y
s . x in Cn X by A2, Def8;
then s . y in Cn X by A1, Th14;
hence X |- s . y by Def8; :: thesis: verum