for A being Element of MP-WFF holds P₁[A]

A1: P₁[ VERUM ] and
A2: for p being MP-variable holds P₁[ @ p] and
A3: for A being Element of MP-WFF st P₁[A] holds
P₁[ 'not' A] and
A4: for A being Element of MP-WFF st P₁[A] holds
P₁[ (#) A] and
A5: for A, B being Element of MP-WFF st P₁[A] & P₁[B] holds
P₁[A '&' B]