consider n being Element of NAT such that
A3: n > 1 and
A4: P₁[n] by A1;
n >= 1 + 1 by A3, NAT_1:13;
then A5: ( P₁[n] & n >= 2 ) by A4;
A6: for k being Element of NAT st 1 <= k & k < n & P₁[k + 1] holds
P₁[k] by A2;
for k being Element of NAT st 1 <= k & k <= n holds
P₁[k] from HALLMAR1:sch 1(A5, A6);
hence P₁[1] by A3; :: thesis: verum