let A be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF A)
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st X |- p holds
X |- All (x,p)
let X be Subset of (CQC-WFF A); :: thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A st X |- p holds
X |- All (x,p)
let p be Element of CQC-WFF A; :: thesis: for x being bound_QC-variable of A st X |- p holds
X |- All (x,p)
let x be bound_QC-variable of A; :: 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