let M be Cardinal; :: thesis:
defpred S₁[ Ordinal] means ( $1 is Cardinal implies P₁[$1] );
A2: for A being Ordinal st ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

let A be Ordinal; :: thesis:
assume A3: for B being Ordinal st B in A & B is Cardinal holds
P₁[B] ; :: thesis:
assume A is Cardinal ; :: thesis:
then reconsider M = A as Cardinal ;
for N being Cardinal st N in M holds
P₁[N] by A3;
hence P₁[A] by A1; :: thesis:

end;