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

A1: P₁[ FaLSUM ] and
A2: for n being Element of NAT holds P₁[ Prop n] and
A3: for r, s being Element of PL-WFF st P₁[r] & P₁[s] holds
P₁[r => s]