let p be Element of CQC-WFF F₁(); :: thesis: P₁[p]
defpred S₁[ Nat] means for p being Element of CQC-WFF F₁() st QuantNbr p <= $1 holds
P₁[p];
A3: for k being Nat st S₁[k] holds
S₁[k + 1] by A2;
A4: S₁[ 0 ] by A1;
for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A3);
then S₁[ QuantNbr p] ;
hence P₁[p] ; :: thesis: verum