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

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] )