let M be Cardinal; :: thesis: P₁[M]
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]

proof

let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume A3: for B being Ordinal st B in A & B is Cardinal holds
P₁[B] ; :: thesis: S₁[A]
assume A is Cardinal ; :: thesis: P₁[A]
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: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A2);
hence P₁[M] ; :: thesis: verum