let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds X |- (All (x,p)) => p
let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds X |- (All (x,p)) => p
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al holds X |- (All (x,p)) => p
let x be bound_QC-variable of Al; :: thesis: X |- (All (x,p)) => p
(All (x,p)) => p in Cn X by Th12;
hence X |- (All (x,p)) => p by Def8; :: thesis: verum