let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable st p is valid holds
All x,p is valid
let x be bound_QC-variable; :: thesis: ( p is valid implies All x,p is valid )
A1: p => (((All x,p) => (All x,p)) => p) is valid ;
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 p is valid ; :: thesis: All x,p is valid
then ((All x,p) => (All x,p)) => p is valid by A1, CQC_THE1:104;
then ((All x,p) => (All x,p)) => (All x,p) is valid by A2, CQC_THE1:106;
hence All x,p is valid by CQC_THE1:104; :: thesis: verum