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 that
A1: X |- p => q and
A2: not x in still_not-bound_in p ; :: thesis: X |- p => (All (x,q))
p => q in Cn X by A1, Def9;
then p => (All (x,q)) in Cn X by A2, Th34;
hence X |- p => (All (x,q)) by Def9; :: thesis: verum