let X be Subset of CQC-WFF; :: thesis: for p being Element of CQC-WFF
for x being bound_QC-variable st X |- p holds
X |- All (x,p)
let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable st X |- p holds
X |- All (x,p)
let x be bound_QC-variable; :: thesis: ( X |- p implies X |- All (x,p) )
A1: X |- p => (((All (x,p)) => (All (x,p))) => p) by CQC_THE1:59;
not x in still_not-bound_in (All (x,p)) by Th5;
then A2: not x in still_not-bound_in ((All (x,p)) => (All (x,p))) by Th7;
assume X |- p ; :: thesis: X |- All (x,p)
then X |- ((All (x,p)) => (All (x,p))) => p by A1, CQC_THE1:55;
then A3: X |- ((All (x,p)) => (All (x,p))) => (All (x,p)) by A2, CQC_THE1:57;
X |- (All (x,p)) => (All (x,p)) by CQC_THE1:59;
hence X |- All (x,p) by A3, CQC_THE1:55; :: thesis: verum