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 )
assume A1: p is valid ; :: thesis: All x,p is valid
p => (((All x,p) => (All x,p)) => p) is valid by LUKASI_1:45;
then A2: ((All x,p) => (All x,p)) => p is valid by A1, CQC_THE1:104;
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 ( ((All x,p) => (All x,p)) => (All x,p) is valid & (All x,p) => (All x,p) is valid ) by A2, CQC_THE1:106, LUKASI_1:44;
hence All x,p is valid by CQC_THE1:104; :: thesis: verum