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 )
assume A1: X |- p ; :: thesis: X |- All x,p
X |- p => (((All x,p) => (All x,p)) => p) by CQC_THE1:98, LUKASI_1:45;
then A2: X |- ((All x,p) => (All x,p)) => p by A1, CQC_THE1:92;
not x in still_not-bound_in (All x,p) by Th5;
then not x in still_not-bound_in ((All x,p) => (All x,p)) by Th7;
then A3: X |- ((All x,p) => (All x,p)) => (All x,p) by A2, CQC_THE1:94;
X |- (All x,p) => (All x,p) by CQC_THE1:98, LUKASI_1:44;
hence X |- All x,p by A3, CQC_THE1:92; :: thesis: verum