let X be Subset of CQC-WFF ; :: thesis: for p, q being Element of CQC-WFF
for x being bound_QC-variable st X |- p => q & not x in still_not-bound_in p holds
X |- p => (All x,q)
let p, q be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable st X |- p => q & not x in still_not-bound_in p holds
X |- p => (All x,q)
let x be bound_QC-variable; :: thesis: ( X |- p => q & not x in still_not-bound_in p implies X |- p => (All x,q) )
assume ( X |- p => q & not x in still_not-bound_in p ) ; :: thesis: X |- p => (All x,q)
then ( p => q in Cn X & not x in still_not-bound_in p ) by Def9;
then p => (All x,q) in Cn X by Th34;
hence X |- p => (All x,q) by Def9; :: thesis: verum