scheme :: HILBERT2:sch 2
HPInd{ P₁[ set ] } :

for r being Element of HP-WFF holds P₁[r]

provided

A1: P₁[ VERUM ] and
A2: for n being Element of NAT holds P₁[ prop n] and
A3: for r, s being Element of HP-WFF st P₁[r] & P₁[s] holds
( P₁[r '&' s] & P₁[r => s] )