let x be bound_QC-variable; :: thesis: for p being Element of QC-WFF holds (All x,p) . x = All x,p
let p be Element of QC-WFF ; :: thesis: (All x,p) . x = All x,p
set q = All x,p;
A1: All x,p is universal by QC_LANG1:def 20;
then bound_in (All x,p) = x by QC_LANG1:def 26;
hence (All x,p) . x = All x,p by A1, Th35; :: thesis: verum