for M being Cardinal holds P₁[M]

A1: P₁[ {} ] and
A2: for M being Cardinal st P₁[M] holds
P₁[ nextcard M] and
A3: for M being Cardinal st M <> {} & M is limit_cardinal & ( for N being Cardinal st N in M holds
P₁[N] ) holds
P₁[M]