let p be Element of CQC-WFF F_{1}(); :: thesis: P_{1}[p]

defpred S_{1}[ Nat] means for p being Element of CQC-WFF F_{1}() st QuantNbr p = $1 holds

P_{1}[p];

A3: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
by A2;

A4: S_{1}[ 0 ]
by A1;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A4, A3);

then S_{1}[ QuantNbr p]
;

hence P_{1}[p]
; :: thesis: verum

defpred S

P

A3: for k being Nat st S

S

A4: S

for k being Nat holds S

then S

hence P